1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Johannes Hölzl, Yury Kudryashov
  5  
  6  Extended non-negative reals
  7  -/
  8  import data.real.nnreal order.bounds data.set.intervals tactic.norm_num
src         └──────────────┘ └──────────┘ └────────────────┘ └─────────────┘
  9  noncomputable theory
 10  open classical set lattice
 11  
 12  open_locale classical
 13  variables {α : Type*} {β : Type*}
 14  
 15  /-- The extended nonnegative real numbers. This is usually denoted [0, ∞],
 16    and is relevant as the codomain of a measure. -/
 17  @[derive canonically_ordered_comm_semiring, derive complete_linear_order, derive densely_ordered]
id            └───────────────────────────────┘         └───────────────────┘         └─────────────┘
src           └───────────────────────────────┘         └───────────────────┘         └─────────────┘
typ           └───────────────────────────────┘         └───────────────────┘         └─────────────┘
doc    └────┘                                    └────┘ └───────────────────┘  └────┘ └─────────────┘
 18  def ennreal := with_top nnreal
id                  └──────┘ └────┘
src                 └──────┘ └────┘
typ                 └──────┘ └────┘
doc                          └────┘
 19  
 20  localized "notation `∞` := (⊤ : ennreal)" in ennreal
 21  
 22  namespace ennreal
 23  variables {a b c d : ennreal} {r p q : nnreal}
id                        └─────┘           └────┘
src                       └─────┘           └────┘
typ                       └─────┘           └────┘
doc                       └─────┘           └────┘
 24  
 25  instance : inhabited ennreal := ⟨0⟩
id              └───────┘ └─────┘
src             └───────┘ └─────┘
typ             └───────┘ └─────┘
doc                       └─────┘
 26  
 27  instance : has_coe nnreal ennreal := ⟨ option.some ⟩
id              └─────┘ └────┘ └─────┘      └─────────┘
src             └─────┘ └────┘ └─────┘      └─────────┘
typ             └─────┘ └────┘ └─────┘      └─────────┘
doc                     └────┘ └─────┘
 28  
 29  instance : can_lift ennreal nnreal :=
id              └──────┘ └─────┘ └────┘
src             └──────┘ └─────┘ └────┘
typ             └──────┘ └─────┘ └────┘
doc             └──────┘ └─────┘ └────┘
 30  { coe := coe,
id            └─┘
src           └─┘
typ           └─┘
 31    cond := λ r, r ≠ ∞,
id                   
src                    
typ                  
doc                     
 32    prf := λ x hx, ⟨option.get $ option.ne_none_iff_is_some.1 hx, option.some_get _⟩ }
id               └┘   └────────┘   └────────────────────────┘  └┘  └─────────────┘
src                    └────────┘   └────────────────────────┘      └─────────────┘
typ              └┘   └────────┘   └────────────────────────┘  └┘  └─────────────┘
 33  
 34  lemma none_eq_top : (none : ennreal) = (⊤ : ennreal) := rfl
id                        └──┘   └─────┘       └─────┘     └─┘
src                       └──┘   └─────┘       └─────┘     └─┘
typ                       └──┘   └─────┘       └─────┘     └─┘
doc                              └─────┘         └─────┘
 35  lemma some_eq_coe (a : nnreal) : (some a : ennreal) = (↑a : ennreal) := rfl
id                          └────┘     └──┘    └─────┘       └─────┘     └─┘
src                         └────┘     └──┘     └─────┘        └─────┘     └─┘
typ                         └────┘     └──┘    └─────┘       └─────┘     └─┘
doc                         └────┘              └─────┘          └─────┘
 36  
 37  /-- `to_nnreal x` returns `x` if it is real, otherwise 0. -/
 38  protected def to_nnreal : ennreal → nnreal
id                             └─────┘  └────┘
src                            └─────┘   └────┘
typ                            └─────┘  └────┘
doc                            └─────┘   └────┘
 39  | (some r) := r
id      └──┘ 
src     └──┘
typ     └──┘ 
 40  | none := 0
id     └──┘
src    └──┘
typ    └──┘
 41  
 42  /-- `to_real x` returns `x` if it is real, `0` otherwise. -/
 43  protected def to_real (a : ennreal) : real := coe (a.to_nnreal)
id                              └─────┘    └──┘    └─┘  └────────┘
src                             └─────┘    └──┘    └─┘   └────────┘
typ                             └─────┘    └──┘    └─┘  └────────┘
doc                             └─────┘                  └────────┘
 44  
 45  /-- `of_real x` returns `x` if it is nonnegative, `0` otherwise. -/
 46  protected def of_real (r : real) : ennreal := coe (nnreal.of_real r)
id                              └──┘    └─────┘    └─┘  └────────────┘ 
src                             └──┘    └─────┘    └─┘  └────────────┘
typ                             └──┘    └─────┘    └─┘  └────────────┘ 
doc                                     └─────┘
 47  
 48  @[simp, elim_cast] lemma to_nnreal_coe : (r : ennreal).to_nnreal = r := rfl
id                                                └─────┘ └───────┘       └─┘
src                                                └─────┘ └───────┘        └─┘
typ                                               └─────┘ └───────┘       └─┘
doc    └──┘  └───────┘                             └─────┘ └───────┘
 49  
 50  @[simp] lemma coe_to_nnreal : ∀{a:ennreal}, a ≠ ∞ → ↑(a.to_nnreal) = a
id                                    └─────┘         └────────┘   
src                                    └─────┘           └────────┘  
typ                                   └─────┘         └────────┘   
doc    └──┘                            └─────┘             └────────┘
 51  | (some r) h := rfl
id      └──┘         └─┘
src     └──┘         └─┘
typ     └──┘         └─┘
 52  | none     h := (h rfl).elim
id     └──┘            └─┘ └──┘
src    └──┘             └─┘ └──┘
typ    └──┘            └─┘ └──┘
 53  
 54  @[simp] lemma of_real_to_real {a : ennreal} (h : a ≠ ∞) : ennreal.of_real (a.to_real) = a :=
id                                      └─────┘             └─────────────┘  └──────┘   
src                                     └─────┘              └─────────────┘   └──────┘  
typ                                     └─────┘             └─────────────┘  └──────┘   
doc    └──┘                             └─────┘               └─────────────┘   └──────┘
 55  by simp [ennreal.to_real, ennreal.of_real, h]
id            └─────────────┘  └─────────────┘  
src     └────┘└─────────────┘└┘└─────────────┘└┘ └─
typ     └────┘└─────────────┘└┘└─────────────┘└┘└─
doc     └────┘└─────────────┘└┘└─────────────┘└┘ └─
txt     └────┘               └┘               └┘ └─
par     └────┘               └┘               └┘ └─
pid                        └┘               └┘ 
st     └───────────────────────────────────────────
 56  
src  
typ  
doc  
txt  
par  
pid  
st   
 57  @[simp] lemma to_real_of_real {r : real} (h : 0 ≤ r) : ennreal.to_real (ennreal.of_real r) = r :=
id                                      └──┘              └─────────────┘  └─────────────┘    
src                                     └──┘               └─────────────┘  └─────────────┘    
typ                                     └──┘              └─────────────┘  └─────────────┘    
doc    └──┘                                                 └─────────────┘  └─────────────┘
 58  by simp [ennreal.to_real, ennreal.of_real, nnreal.coe_of_real _ h]
id            └─────────────┘  └─────────────┘  └────────────────┘   
src     └────┘└─────────────┘└┘└─────────────┘└┘└────────────────┘└─┘ └─
typ     └────┘└─────────────┘└┘└─────────────┘└┘└────────────────┘└─┘└─
doc     └────┘└─────────────┘└┘└─────────────┘└┘                  └─┘ └─
txt     └────┘               └┘               └┘                  └─┘ └─
par     └────┘               └┘               └┘                  └─┘ └─
pid                        └┘               └┘                  └─┘ 
st     └────────────────────────────────────────────────────────────────
 59  
src  
typ  
doc  
txt  
par  
pid  
st   
 60  lemma coe_to_nnreal_le_self : ∀{a:ennreal}, ↑(a.to_nnreal) ≤ a
id                                    └─────┘    └────────┘   
src                                    └─────┘     └────────┘  
typ                                   └─────┘    └────────┘   
doc                                    └─────┘      └────────┘
 61  | (some r) := by rw [some_eq_coe, to_nnreal_coe]; exact le_refl _
id      └──┘              └─────────┘  └───────────┘         └─────┘
src     └──┘          └──┘└─────────┘└┘└───────────┘  └────┘└─────┘└─┘
typ     └──┘          └──┘└─────────┘└┘└───────────┘  └────┘└─────┘└─┘
doc                   └──┘           └┘               └────┘       └─┘
txt                   └──┘           └┘               └────┘       └─┘
par                   └──┘           └┘               └────┘       └─┘
pid                     └┘           └┘                           └┘
st                   └──────────────┘└─────────────┘└────────────────┘
 62  | none     := le_top
id     └──┘        └────┘
src    └──┘        └────┘
typ    └──┘        └────┘
 63  
 64  lemma coe_nnreal_eq (r : nnreal) : (r : ennreal) = ennreal.of_real r :=
id                            └────┘        └─────┘   └─────────────┘ 
src                           └────┘         └─────┘   └─────────────┘
typ                           └────┘        └─────┘   └─────────────┘ 
doc                           └────┘         └─────┘    └─────────────┘
 65  by { rw [ennreal.of_real, nnreal.of_real], cases r with r h, congr, dsimp, rw max_eq_left h }
id            └─────────────┘  └────────────┘                                     └─────────┘ 
src       └──┘└─────────────┘└┘└────────────┘  └────┘ └───────┘  └───┘  └───┘  └─┘└─────────┘ 
typ       └──┘└─────────────┘└┘└────────────┘  └────┘└───────┘  └───┘  └───┘  └─┘└─────────┘
doc       └──┘└─────────────┘└┘                └────┘ └───────┘         └───┘  └─┘            
txt       └──┘               └┘                └────┘ └───────┘  └───┘  └───┘  └─┘            
par       └──┘               └┘                └────┘ └───────┘  └───┘  └───┘  └─┘            
pid         └┘               └┘                      └───────┘                              
st     └────────────────────┘└──────────────┘└─────────────────┘└─────┘└─────┘└─────────────────┘└┘
 66  
 67  lemma of_real_eq_coe_nnreal {x : real} (h : 0 ≤ x) :
id                                    └──┘          
src                                   └──┘         
typ                                   └──┘          
 68    ennreal.of_real x = @coe nnreal ennreal _ (⟨x, h⟩ : nnreal) :=
id     └─────────────┘    └─┘ └────┘ └─────┘           └────┘
src    └─────────────┘     └─┘ └────┘ └─────┘             └────┘
typ    └─────────────┘    └─┘ └────┘ └─────┘           └────┘
doc    └─────────────┘          └────┘ └─────┘             └────┘
 69  by { rw [coe_nnreal_eq], refl }
id            └───────────┘
src       └──┘└───────────┘  └───┘
typ       └──┘└───────────┘  └───┘
doc       └──┘               └───┘
txt       └──┘               └───┘
par       └──┘               └───┘
pid         └┘                   
st     └──────────────────┘└──────┘└┘
 70  
 71  @[simp, elim_cast] lemma coe_zero : ↑(0 : nnreal) = (0 : ennreal) := rfl
id                                            └────┘        └─────┘     └─┘
src                                           └────┘        └─────┘     └─┘
typ                                           └────┘        └─────┘     └─┘
doc    └──┘  └───────┘                         └────┘         └─────┘
 72  @[simp, elim_cast] lemma coe_one : ↑(1 : nnreal) = (1 : ennreal) := rfl
id                                           └────┘        └─────┘     └─┘
src                                          └────┘        └─────┘     └─┘
typ                                          └────┘        └─────┘     └─┘
doc    └──┘  └───────┘                        └────┘         └─────┘
 73  
 74  @[simp] lemma to_real_nonneg {a : ennreal} : 0 ≤ a.to_real := by simp [ennreal.to_real]
id                                     └─────┘       └──────┘             └─────────────┘
src                                    └─────┘        └──────┘       └────┘└─────────────┘└─
typ                                    └─────┘       └──────┘       └────┘└─────────────┘└─
doc    └──┘                            └─────┘         └──────┘       └────┘└─────────────┘└─
txt                                                                   └────┘               └─
par                                                                   └────┘               └─
pid                                                                                      
st                                                                   └───────────────────────
 75  
src  
typ  
doc  
txt  
par  
pid  
st   
 76  @[simp] lemma top_to_nnreal : ∞.to_nnreal = 0 := rfl
id                                 └───────┘        └─┘
src                                └───────┘        └─┘
typ                                └───────┘        └─┘
doc    └──┘                        └───────┘
 77  @[simp] lemma top_to_real : ∞.to_real = 0 := rfl
id                               └─────┘        └─┘
src                              └─────┘        └─┘
typ                              └─────┘        └─┘
doc    └──┘                      └─────┘
 78  @[simp] lemma coe_to_real (r : nnreal) : (r : ennreal).to_real = r := rfl
id                                  └────┘        └─────┘ └─────┘       └─┘
src                                 └────┘         └─────┘ └─────┘        └─┘
typ                                 └────┘        └─────┘ └─────┘       └─┘
doc    └──┘                         └────┘         └─────┘ └─────┘
 79  @[simp] lemma zero_to_nnreal : (0 : ennreal).to_nnreal = 0 := rfl
id                                       └─────┘ └───────┘        └─┘
src                                      └─────┘ └───────┘        └─┘
typ                                      └─────┘ └───────┘        └─┘
doc    └──┘                              └─────┘ └───────┘
 80  @[simp] lemma zero_to_real : (0 : ennreal).to_real = 0 := rfl
id                                     └─────┘ └─────┘        └─┘
src                                    └─────┘ └─────┘        └─┘
typ                                    └─────┘ └─────┘        └─┘
doc    └──┘                            └─────┘ └─────┘
 81  @[simp] lemma of_real_zero : ennreal.of_real (0 : ℝ) = 0 :=
id                                └─────────────┘        
src                               └─────────────┘        
typ                               └─────────────┘        
doc    └──┘                       └─────────────┘
 82  by simp [ennreal.of_real]; refl
id            └─────────────┘
src     └────┘└─────────────┘  └───┘
typ     └────┘└─────────────┘  └───┘
doc     └────┘└─────────────┘  └───┘
txt     └────┘                 └───┘
par     └────┘                 └───┘
pid                              
st     └────────────────────────────┘
 83  @[simp] lemma of_real_one : ennreal.of_real (1 : ℝ) = (1 : ennreal) :=
id                               └─────────────┘              └─────┘
src                              └─────────────┘              └─────┘
typ                              └─────────────┘              └─────┘
doc    └──┘                      └─────────────┘                └─────┘
 84  by simp [ennreal.of_real]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘└─────────────┘└─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
 85  
src  
typ  
doc  
txt  
par  
pid  
st   
 86  lemma of_real_to_real_le {a : ennreal} : ennreal.of_real (a.to_real) ≤ a :=
id                                 └─────┘    └─────────────┘  └──────┘   
src                                └─────┘    └─────────────┘   └──────┘  
typ                                └─────┘    └─────────────┘  └──────┘   
doc                                └─────┘    └─────────────┘   └──────┘
 87  if ha : a = ∞ then ha.symm ▸ le_top else le_of_eq (of_real_to_real ha)
id   └┘              └┘└───┘  └────┘      └──────┘  └─────────────┘ └┘
src  └┘                 └───┘  └────┘      └──────┘  └─────────────┘
typ  └┘              └┘└───┘  └────┘      └──────┘  └─────────────┘ └┘
doc              
 88  
 89  lemma forall_ennreal {p : ennreal → Prop} : (∀a, p a) ↔ (∀r:nnreal, p r) ∧ p ∞ :=
id                             └─────┘                       └────┘       
src                            └─────┘                          └────┘          
typ                            └─────┘                       └────┘       
doc                            └─────┘                           └────┘           
 90  ⟨assume h, ⟨assume r, h _, h _⟩,
id                           
typ                          
 91    assume ⟨h₁, h₂⟩ a, match a with some r := h₁ _ | none := h₂ end⟩
id            └┘  └┘                └──┘             └──┘
src                                    └──┘             └──┘
typ           └┘  └┘                └──┘             └──┘
 92  
 93  lemma to_nnreal_eq_zero_iff (x : ennreal) : x.to_nnreal = 0 ↔ x = 0 ∨ x = ⊤ :=
id                                    └─────┘    └────────┘            
src                                   └─────┘     └────────┘              
typ                                   └─────┘    └────────┘            
doc                                   └─────┘     └────────┘
 94  ⟨begin
st    └─────
 95    cases x,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
 96    { simp [none_eq_top] },
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└─────────────────┘└┘
 97    { have A : some (0:nnreal) = (0:ennreal) := rfl,
id                └──┘    └────┘      └─────┘     └─┘
src      └───────┘└──┘ └┘└────┘└┘ └┘└─────┘└───┘└─┘
typ      └───────┘└──┘ └┘└────┘└┘ └┘└─────┘└───┘└─┘
doc      └───────┘     └┘└────┘└┘  └┘└─────┘└───┘
txt      └───────┘     └┘      └┘  └┘       └───┘
par      └───────┘     └┘      └┘  └┘       └───┘
pid      └────┘└─┘     └┘      └┘  └┘       └──┘
st   ────────────────────────────────────────────────┘└─
 98      simp [ennreal.to_nnreal, A] {contextual := tt} }
id             └───────────────┘                   └┘
src      └────┘└───────────────┘└┘ └┘ └────────────┘└┘└┘
typ      └────┘└───────────────┘└┘└┘ └────────────┘└┘└┘
doc      └────┘└───────────────┘└┘ └┘ └────────────┘  └┘
txt      └────┘                 └┘ └┘ └────────────┘  └┘
par      └────┘                 └┘ └┘ └────────────┘  └┘
pid                           └┘  └────────────┘  
st   ──────────────────────────────────────────────────┘└─
 99  end,
st   ──┘
100  by intro h; cases h; simp [h]⟩
id                             
src     └─────┘  └────┘   └────┘ 
typ     └─────┘  └────┘  └────┘
doc     └─────┘  └────┘   └────┘ 
txt     └─────┘  └────┘   └────┘ 
par     └─────┘  └────┘   └────┘ 
pid          └┘               
st     └─────────────────────────┘
101  
102  lemma to_real_eq_zero_iff (x : ennreal) : x.to_real = 0 ↔ x = 0 ∨ x = ⊤ :=
id                                  └─────┘    └──────┘            
src                                 └─────┘     └──────┘              
typ                                 └─────┘    └──────┘            
doc                                 └─────┘     └──────┘
103  by simp [ennreal.to_real, to_nnreal_eq_zero_iff]
id            └─────────────┘  └───────────────────┘
src     └────┘└─────────────┘└┘└───────────────────┘└─
typ     └────┘└─────────────┘└┘└───────────────────┘└─
doc     └────┘└─────────────┘└┘                     └─
txt     └────┘               └┘                     └─
par     └────┘               └┘                     └─
pid                        └┘                     
st     └──────────────────────────────────────────────
104  
src  
typ  
doc  
txt  
par  
pid  
st   
105  @[simp] lemma coe_ne_top : (r : ennreal) ≠ ∞ := with_top.coe_ne_top
id                                  └─────┘       └─────────────────┘
src                                  └─────┘       └─────────────────┘
typ                                 └─────┘       └─────────────────┘
doc    └──┘                          └─────┘    
106  @[simp] lemma top_ne_coe : ∞ ≠ (r : ennreal) := with_top.top_ne_coe
id                                    └─────┘     └─────────────────┘
src                                    └─────┘     └─────────────────┘
typ                                   └─────┘     └─────────────────┘
doc    └──┘                             └─────┘
107  @[simp] lemma of_real_ne_top {r : ℝ} : ennreal.of_real r ≠ ∞ := by simp [ennreal.of_real]
id                                         └─────────────┘                └─────────────┘
src                                        └─────────────┘           └────┘└─────────────┘└┘
typ                                        └─────────────┘          └────┘└─────────────┘└┘
doc    └──┘                                 └─────────────┘            └────┘└─────────────┘└┘
txt                                                                     └────┘               └┘
par                                                                     └────┘               └┘
pid                                                                                        
st                                                                     └──────────────────────┘
108  @[simp] lemma top_ne_of_real {r : ℝ} : ∞ ≠ ennreal.of_real r := by simp [ennreal.of_real]
id                                           └─────────────┘              └─────────────┘
src                                          └─────────────┘         └────┘└─────────────┘└─
typ                                          └─────────────┘        └────┘└─────────────┘└─
doc    └──┘                                    └─────────────┘         └────┘└─────────────┘└─
txt                                                                     └────┘               └─
par                                                                     └────┘               └─
pid                                                                                        
st                                                                     └───────────────────────
109  
src  
typ  
doc  
txt  
par  
pid  
st   
110  @[simp] lemma zero_ne_top : 0 ≠ ∞ := coe_ne_top
id                                      └────────┘
src                                     └────────┘
typ                                     └────────┘
doc    └──┘                          
111  @[simp] lemma top_ne_zero : ∞ ≠ 0 := top_ne_coe
id                                      └────────┘
src                                     └────────┘
typ                                     └────────┘
doc    └──┘                      
112  
113  @[simp] lemma one_ne_top : 1 ≠ ∞ := coe_ne_top
id                                     └────────┘
src                                    └────────┘
typ                                    └────────┘
doc    └──┘                         
114  @[simp] lemma top_ne_one : ∞ ≠ 1 := top_ne_coe
id                                     └────────┘
src                                    └────────┘
typ                                    └────────┘
doc    └──┘                     
115  
116  @[simp, elim_cast] lemma coe_eq_coe : (↑r : ennreal) = ↑q ↔ r = q := with_top.coe_eq_coe
id                                             └─────┘           └─────────────────┘
src                                             └─────┘              └─────────────────┘
typ                                            └─────┘           └─────────────────┘
doc    └──┘  └───────┘                           └─────┘
117  @[simp, elim_cast] lemma coe_le_coe : (↑r : ennreal) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe
id                                             └─────┘           └─────────────────┘
src                                             └─────┘              └─────────────────┘
typ                                            └─────┘           └─────────────────┘
doc    └──┘  └───────┘                           └─────┘
118  @[simp, elim_cast] lemma coe_lt_coe : (↑r : ennreal) < ↑q ↔ r < q := with_top.coe_lt_coe
id                                             └─────┘           └─────────────────┘
src                                             └─────┘              └─────────────────┘
typ                                            └─────┘           └─────────────────┘
doc    └──┘  └───────┘                           └─────┘
119  lemma coe_mono : monotone (coe : nnreal → ennreal) := λ _ _, coe_le_coe.2
id                    └──────┘  └─┘   └────┘   └─────┘          └────────┘
src                   └──────┘  └─┘   └────┘   └─────┘            └────────┘
typ                   └──────┘  └─┘   └────┘   └─────┘          └────────┘
doc                   └──────┘        └────┘   └─────┘
120  
121  @[simp, elim_cast] lemma coe_eq_zero : (↑r : ennreal) = 0 ↔ r = 0 := coe_eq_coe
id                                              └─────┘             └────────┘
src                                              └─────┘              └────────┘
typ                                             └─────┘             └────────┘
doc    └──┘  └───────┘                            └─────┘
122  @[simp, elim_cast] lemma zero_eq_coe : 0 = (↑r : ennreal) ↔ 0 = r := coe_eq_coe
id                                                 └─────┘          └────────┘
src                                                 └─────┘           └────────┘
typ                                                └─────┘          └────────┘
doc    └──┘  └───────┘                                └─────┘
123  @[simp, elim_cast] lemma coe_eq_one : (↑r : ennreal) = 1 ↔ r = 1 := coe_eq_coe
id                                             └─────┘             └────────┘
src                                             └─────┘              └────────┘
typ                                            └─────┘             └────────┘
doc    └──┘  └───────┘                           └─────┘
124  @[simp, elim_cast] lemma one_eq_coe : 1 = (↑r : ennreal) ↔ 1 = r := coe_eq_coe
id                                                └─────┘          └────────┘
src                                                └─────┘           └────────┘
typ                                               └─────┘          └────────┘
doc    └──┘  └───────┘                               └─────┘
125  @[simp, elim_cast] lemma coe_nonneg : 0 ≤ (↑r : ennreal) ↔ 0 ≤ r := coe_le_coe
id                                                └─────┘          └────────┘
src                                                └─────┘           └────────┘
typ                                               └─────┘          └────────┘
doc    └──┘  └───────┘                               └─────┘
126  @[simp, elim_cast] lemma coe_pos : 0 < (↑r : ennreal) ↔ 0 < r := coe_lt_coe
id                                             └─────┘          └────────┘
src                                             └─────┘           └────────┘
typ                                            └─────┘          └────────┘
doc    └──┘  └───────┘                            └─────┘
127  
128  @[simp, move_cast] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add
id                                                  └─────┘     └──────────────┘
src                                                     └─────┘     └──────────────┘
typ                                                 └─────┘     └──────────────┘
doc    └──┘  └───────┘                                      └─────┘
129  @[simp, move_cast] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul
id                                                  └─────┘     └──────────────┘
src                                                     └─────┘     └──────────────┘
typ                                                 └─────┘     └──────────────┘
doc    └──┘  └───────┘                                      └─────┘
130  
131  @[simp, move_cast] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add
id                                         └──┘     └─────┘   └──┘     └─────┘
src                                        └──┘      └─────┘   └──┘      └─────┘
typ                                        └──┘     └─────┘   └──┘     └─────┘
doc    └──┘  └───────┘                                └─────┘
132  @[simp, move_cast] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1]
id                                         └──┘     └─────┘   └──┘              └──┘
src                                        └──┘      └─────┘   └──┘         └────┘└──┘└┘
typ                                        └──┘     └─────┘   └──┘        └────┘└──┘└┘
doc    └──┘  └───────┘                                └─────┘                 └────┘    └┘
txt                                                                           └────┘    └┘
par                                                                           └────┘    └┘
pid                                                                                   
st                                                                           └───────────┘
133  lemma coe_two : ((2:nnreal) : ennreal) = 2 := by norm_cast
id                       └────┘    └─────┘  
src                      └────┘    └─────┘           └─────────
typ                      └────┘    └─────┘           └─────────
doc                      └────┘    └─────┘            └─────────
txt                                                   └─────────
par                                                   └─────────
pid                                                            
st                                                   └──────────
134  
src  
typ  
doc  
txt  
par  
pid  
st   
135  protected lemma zero_lt_one : 0 < (1 : ennreal) :=
id                                         └─────┘
src                                        └─────┘
typ                                        └─────┘
doc                                         └─────┘
136    canonically_ordered_semiring.zero_lt_one
id     └──────────────────────────────────────┘
src    └──────────────────────────────────────┘
typ    └──────────────────────────────────────┘
doc    └──────────────────────────────────────┘
137  
138  @[simp] lemma one_lt_two : (1:ennreal) < 2 := coe_one ▸ coe_two ▸ by exact_mod_cast one_lt_two
id                                 └─────┘        └─────┘  └─────┘                    └────────┘
src                                └─────┘        └─────┘  └─────┘     └─────────────┘└────────┘
typ                                └─────┘        └─────┘  └─────┘     └─────────────┘└────────┘
doc    └──┘                        └─────┘                                └─────────────┘          
txt                                                                       └─────────────┘          
par                                                                       └─────────────┘          
pid                                                                                               
st                                                                       └─────────────────────────┘
139  @[simp] lemma two_pos : (0:ennreal) < 2 := lt_trans ennreal.zero_lt_one one_lt_two
id                              └─────┘        └──────┘ └─────────────────┘ └────────┘
src                             └─────┘        └──────┘ └─────────────────┘ └────────┘
typ                             └─────┘        └──────┘ └─────────────────┘ └────────┘
doc    └──┘                     └─────┘
140  @[simp] lemma two_ne_zero : (2:ennreal) ≠ 0 := ne_of_gt two_pos
id                                  └─────┘        └──────┘ └─────┘
src                                 └─────┘        └──────┘ └─────┘
typ                                 └─────┘        └──────┘ └─────┘
doc    └──┘                         └─────┘
141  @[simp] lemma two_ne_top : (2:ennreal) ≠ ∞ := coe_two ▸ coe_ne_top
id                                 └─────┘       └─────┘  └────────┘
src                                └─────┘       └─────┘  └────────┘
typ                                └─────┘       └─────┘  └────────┘
doc    └──┘                        └─────┘    
142  
143  @[simp] lemma add_top : a + ∞ = ∞ := with_top.add_top
id                                   └──────────────┘
src                                   └──────────────┘
typ                                  └──────────────┘
doc    └──┘                         
144  @[simp] lemma top_add : ∞ + a = ∞ := with_top.top_add
id                                   └──────────────┘
src                                   └──────────────┘
typ                                  └──────────────┘
doc    └──┘                         
145  
146  instance : is_semiring_hom (coe : nnreal → ennreal) :=
id              └─────────────┘  └─┘   └────┘   └─────┘
src             └─────────────┘  └─┘   └────┘   └─────┘
typ             └─────────────┘  └─┘   └────┘   └─────┘
doc             └─────────────┘        └────┘   └─────┘
147  by refine_struct {..}; simp
src     └────────────┘ └─┘  └────
typ     └────────────┘ └─┘  └────
doc     └────────────┘ └─┘  └────
txt     └────────────┘ └─┘  └────
par     └────────────┘ └─┘  └────
pid                   └─┘      
st     └─────────────────────────
148  
src  
typ  
doc  
txt  
par  
pid  
st   
149  @[simp, move_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ennreal) = r^n :=
id                                                   └─────┘   
src                                                    └─────┘    
typ                                                  └─────┘   
doc    └──┘  └───────┘                                    └─────┘
150  is_monoid_hom.map_pow coe r n
id   └───────────────────┘ └─┘  
src  └───────────────────┘ └─┘
typ  └───────────────────┘ └─┘  
151  
152  lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _
id                                      └─────────────────┘
src                                         └─────────────────┘
typ                                     └─────────────────┘
doc                                           
153  lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _
id                                      └─────────────────┘
src                                         └─────────────────┘
typ                                     └─────────────────┘
doc                                           
154  
155  lemma to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ < ⊤) (h₂ : r₂ < ⊤) :
id                                └─────┘        └┘          └┘  
src                               └─────┘                        
typ                               └─────┘        └┘          └┘  
doc                               └─────┘
156    (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal :=
id      └┘  └┘ └───────┘   └┘└────────┘  └┘└────────┘
src            └───────┘     └────────┘    └────────┘
typ     └┘  └┘ └───────┘   └┘└────────┘  └┘└────────┘
doc             └───────┘      └────────┘     └────────┘
157  begin
st   └─────
158    rw [← coe_eq_coe, coe_add, coe_to_nnreal, coe_to_nnreal, coe_to_nnreal];
id           └────────┘  └─────┘  └───────────┘  └───────────┘  └───────────┘
src    └────┘└────────┘└┘└─────┘└┘└───────────┘└┘└───────────┘└┘└───────────┘
typ    └────┘└────────┘└┘└─────┘└┘└───────────┘└┘└───────────┘└┘└───────────┘
doc    └────┘          └┘       └┘             └┘             └┘             
txt    └────┘          └┘       └┘             └┘             └┘             
par    └────┘          └┘       └┘             └┘             └┘             
pid      └──┘          └┘       └┘             └┘             └┘             
st   ─────────────────┘└───────┘└─────────────┘└─────────────┘└─────────────┘└─
159      apply @ne_top_of_lt ennreal _ _ ⊤,
id              └──────────┘ └─────┘     
src      └────┘ └──────────┘└─────┘└───┘
typ      └────┘ └──────────┘└─────┘└───┘
doc      └────┘             └─────┘└───┘
txt      └────┘                    └───┘
par      └────┘                    └───┘
pid                               └───┘
st   ────────────────────────────────────┘└─
160    exact h₂,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
161    exact h₁,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
162    exact add_lt_top.2 ⟨h₁, h₂⟩
id           └────────┘    └┘  └┘
src    └────┘└────────┘└─┘   └┘  └┘
typ    └────┘└────────┘└─┘ └┘└┘└┘└┘
doc    └────┘          └─┘   └┘  └┘
txt    └────┘          └─┘   └┘  └┘
par    └────┘          └─┘   └┘  └┘
pid                   └─┘   └┘  
st   ─────────────────────────────┘
163  end
st   └─┘
164  
165  /- rw has trouble with the generic lt_top_iff_ne_top and bot_lt_iff_ne_bot
166  (contrary to erw). This is solved with the next lemmas -/
167  protected lemma lt_top_iff_ne_top : a < ∞ ↔ a ≠ ∞ := lt_top_iff_ne_top
id                                                 └───────────────┘
src                                                  └───────────────┘
typ                                                └───────────────┘
doc                                                 
168  protected lemma bot_lt_iff_ne_bot : 0 < a ↔ a ≠ 0 := bot_lt_iff_ne_bot
id                                                   └───────────────┘
src                                                    └───────────────┘
typ                                                  └───────────────┘
169  
170  lemma add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ :=
id                                  
src                                     
typ                                 
doc                                           
171  by simpa only [lt_top_iff_ne_top] using add_lt_top
id                  └───────────────┘        └────────┘
src     └──────────┘└───────────────┘└──────┘└────────┘
typ     └──────────┘└───────────────┘└──────┘└────────┘
doc     └──────────┘                 └──────┘          
txt     └──────────┘                 └──────┘          
par     └──────────┘                 └──────┘          
pid          └──┘└┘                 └────┘          
st     └────────────────────────────────────────────────
172  
src  
typ  
doc  
txt  
par  
pid  
st   
173  lemma mul_top : a * ∞ = (if a = 0 then 0 else ∞) :=
id                                           
src                                            
typ                                          
doc                                               
174  begin split_ifs, { simp [h] }, { exact with_top.mul_top h } end
id                                         └──────────────┘ 
src        └───────┘    └────┘ └┘     └────┘└──────────────┘ 
typ        └───────┘    └────┘└┘     └────┘└──────────────┘
doc        └───────┘    └────┘ └┘     └────┘                 
txt        └───────┘    └────┘ └┘     └────┘                 
par        └───────┘    └────┘ └┘     └────┘                 
pid                                                     
st   └─────────────┘└──┘└───────┘└┘└──────────────────────────┘└───┘
175  
176  lemma top_mul : ∞ * a = (if a = 0 then 0 else ∞) :=
id                                           
src                                            
typ                                          
doc                                               
177  begin split_ifs, { simp [h] }, { exact with_top.top_mul h } end
id                                         └──────────────┘ 
src        └───────┘    └────┘ └┘     └────┘└──────────────┘ 
typ        └───────┘    └────┘└┘     └────┘└──────────────┘
doc        └───────┘    └────┘ └┘     └────┘                 
txt        └───────┘    └────┘ └┘     └────┘                 
par        └───────┘    └────┘ └┘     └────┘                 
pid                                                     
st   └─────────────┘└──┘└───────┘└┘└──────────────────────────┘└───┘
178  
179  @[simp] lemma top_mul_top : ∞ * ∞ = ∞ := with_top.top_mul_top
id                                       └──────────────────┘
src                                      └──────────────────┘
typ                                      └──────────────────┘
doc    └──┘                            
180  
181  lemma top_pow {n:ℕ} (h : 0 < n) : ∞^n = ∞ :=
id                                    
src                                     
typ                                   
doc                                         
182  nat.le_induction (pow_one _) (λ m hm hm', by rw [pow_succ, hm', top_mul_top])
id   └──────────────┘  └─────┘        └┘ └─┘         └──────┘  └─┘  └─────────┘
src  └──────────────┘  └─────┘                    └──┘└──────┘└┘   └┘└─────────┘
typ  └──────────────┘  └─────┘        └┘ └─┘     └──┘└──────┘└┘└─┘└┘└─────────┘
doc  └──────────────┘                             └──┘        └┘   └┘           
txt                                               └──┘        └┘   └┘           
par                                               └──┘        └┘   └┘           
pid                                                 └┘        └┘   └┘           
st                                               └───────────┘└───┘└───────────┘
183    _ (nat.succ_le_of_lt h)
id        └───────────────┘ 
src       └───────────────┘
typ       └───────────────┘ 
184  
185  lemma mul_eq_top {a b : ennreal} : a * b = ⊤ ↔ (a ≠ 0 ∧ b = ⊤) ∨ (a = ⊤ ∧ b ≠ 0) :=
id                           └─────┘                           
src                          └─────┘                                 
typ                          └─────┘                           
doc                          └─────┘
186  with_top.mul_eq_top_iff
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
187  
188  lemma mul_ne_top {a b : ennreal} : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ :=
id                           └─────┘                  
src                          └─────┘                      
typ                          └─────┘                  
doc                          └─────┘                          
189  by simp [(≠), mul_eq_top] {contextual := tt}
id                └────────┘                 └┘
src     └────┘└──┘└────────┘└┘ └────────────┘└┘└─
typ     └────┘└──┘└────────┘└┘ └────────────┘└┘└─
doc     └────┘ └──┘          └┘ └────────────┘  └─
txt     └────┘ └──┘          └┘ └────────────┘  └─
par     └────┘ └──┘          └┘ └────────────┘  └─
pid          └──┘           └────────────┘  
st     └──────────────────────────────────────────
190  
src  
typ  
doc  
txt  
par  
pid  
st   
191  lemma mul_lt_top {a b : ennreal}  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
id                           └─────┘                   
src                          └─────┘                       
typ                          └─────┘                   
doc                          └─────┘
192  by simpa only [ennreal.lt_top_iff_ne_top] using mul_ne_top
id                  └───────────────────────┘        └────────┘
src     └──────────┘└───────────────────────┘└──────┘└────────┘
typ     └──────────┘└───────────────────────┘└──────┘└────────┘
doc     └──────────┘                         └──────┘          
txt     └──────────┘                         └──────┘          
par     └──────────┘                         └──────┘          
pid          └──┘└┘                         └────┘          
st     └────────────────────────────────────────────────────────
193  
src  
typ  
doc  
txt  
par  
pid  
st   
194  lemma pow_eq_top : ∀ n:ℕ, a^n=∞ → a=∞
id                              
src                                 
typ                             
doc                                     
195  | 0 := by simp
src            └───┘
typ            └───┘
doc            └───┘
txt            └───┘
par            └───┘
pid                
st            └────┘
196  | (n+1) := λ o, (mul_eq_top.1 o).elim (λ h, pow_eq_top n h.2) and.left
id                 └────────┘   └──┘       └────────┘      └──────┘
src                  └────────┘    └──┘                         └──────┘
typ                └────────┘   └──┘       └────────┘      └──────┘
197  
198  lemma pow_ne_top (h : a ≠ ∞) {n:ℕ} : a^n ≠ ∞ :=
id                                      
src                                        
typ                                     
doc                                            
199  mt (pow_eq_top n) h
id   └┘  └────────┘   
src  └┘  └────────┘
typ  └┘  └────────┘   
200  
201  lemma pow_lt_top : a < ∞ → ∀ n:ℕ, a^n < ∞ :=
id                                   
src                                     
typ                                  
doc                                         
202  by simpa only [lt_top_iff_ne_top] using pow_ne_top
id                  └───────────────┘        └────────┘
src     └──────────┘└───────────────┘└──────┘└────────┘
typ     └──────────┘└───────────────┘└──────┘└────────┘
doc     └──────────┘                 └──────┘          
txt     └──────────┘                 └──────┘          
par     └──────────┘                 └──────┘          
pid          └──┘└┘                 └────┘          
st     └────────────────────────────────────────────────
203  
src  
typ  
doc  
txt  
par  
pid  
st   
204  @[simp, move_cast] lemma coe_finset_sum {s : finset α} {f : α → nnreal} :
id                                                └────┘           └────┘
src                                               └────┘             └────┘
typ                                               └────┘           └────┘
doc    └──┘  └───────┘                            └────┘             └────┘
205    ↑(s.sum f) = (s.sum (λa, f a) : ennreal) :=
id      └──┘     └──┘          └─────┘
src      └──┘       └──┘             └─────┘
typ     └──┘     └──┘          └─────┘
doc                                    └─────┘
206  (s.sum_hom coe).symm
id    └──────┘ └─┘ └──┘
src    └──────┘ └─┘ └──┘
typ   └──────┘ └─┘ └──┘
207  
208  @[simp, move_cast] lemma coe_finset_prod {s : finset α} {f : α → nnreal} :
id                                                 └────┘           └────┘
src                                                └────┘             └────┘
typ                                                └────┘           └────┘
doc    └──┘  └───────┘                             └────┘             └────┘
209    ↑(s.prod f) = (s.prod (λa, f a) : ennreal) :=
id      └───┘     └───┘          └─────┘
src      └───┘       └───┘             └─────┘
typ     └───┘     └───┘          └─────┘
doc       └───┘        └───┘             └─────┘
210  (s.prod_hom coe).symm
id    └───────┘ └─┘ └──┘
src    └───────┘ └─┘ └──┘
typ   └───────┘ └─┘ └──┘
211  
212  section order
213  
214  @[simp] lemma bot_eq_zero : (⊥ : ennreal) = 0 := rfl
id                                   └─────┘        └─┘
src                                  └─────┘        └─┘
typ                                  └─────┘        └─┘
doc    └──┘                           └─────┘
215  
216  @[simp] lemma coe_lt_top : coe r < ∞ := with_top.coe_lt_top r
id                              └─┘       └─────────────────┘ 
src                             └─┘        └─────────────────┘
typ                             └─┘       └─────────────────┘ 
doc    └──┘                             
217  @[simp] lemma not_top_le_coe : ¬ (⊤:ennreal) ≤ ↑r := with_top.not_top_le_coe r
id                                     └─────┘       └─────────────────────┘ 
src                                    └─────┘        └─────────────────────┘
typ                                    └─────┘       └─────────────────────┘ 
doc    └──┘                              └─────┘
218  @[simp, elim_cast] lemma zero_lt_coe_iff : 0 < (↑p : ennreal) ↔ 0 < p := coe_lt_coe
id                                                     └─────┘          └────────┘
src                                                     └─────┘           └────────┘
typ                                                    └─────┘          └────────┘
doc    └──┘  └───────┘                                    └─────┘
219  @[simp, elim_cast] lemma one_le_coe_iff : (1:ennreal) ≤ ↑r ↔ 1 ≤ r := coe_le_coe
id                                                └─────┘            └────────┘
src                                               └─────┘              └────────┘
typ                                               └─────┘            └────────┘
doc    └──┘  └───────┘                            └─────┘
220  @[simp, elim_cast] lemma coe_le_one_iff : ↑r ≤ (1:ennreal) ↔ r ≤ 1 := coe_le_coe
id                                                  └─────┘          └────────┘
src                                                  └─────┘           └────────┘
typ                                                 └─────┘          └────────┘
doc    └──┘  └───────┘                                 └─────┘
221  @[simp, elim_cast] lemma coe_lt_one_iff : (↑p : ennreal) < 1 ↔ p < 1 := coe_lt_coe
id                                                 └─────┘             └────────┘
src                                                 └─────┘              └────────┘
typ                                                └─────┘             └────────┘
doc    └──┘  └───────┘                               └─────┘
222  @[simp, elim_cast] lemma one_lt_coe_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe
id                                                    └─────┘          └────────┘
src                                                    └─────┘           └────────┘
typ                                                   └─────┘          └────────┘
doc    └──┘  └───────┘                                   └─────┘
223  @[simp, squash_cast] lemma coe_nat (n : nat) : ((n : nnreal) : ennreal) = n := with_top.coe_nat n
id                                           └─┘         └────┘    └─────┘       └──────────────┘ 
src                                          └─┘          └────┘    └─────┘        └──────────────┘
typ                                          └─┘         └────┘    └─────┘       └──────────────┘ 
doc    └──┘  └─────────┘                                  └────┘    └─────┘
224  @[simp] lemma nat_ne_top (n : nat) : (n : ennreal) ≠ ⊤ := with_top.nat_ne_top n
id                                 └─┘        └─────┘       └─────────────────┘ 
src                                └─┘         └─────┘       └─────────────────┘
typ                                └─┘        └─────┘       └─────────────────┘ 
doc    └──┘                                    └─────┘
225  @[simp] lemma top_ne_nat (n : nat) : (⊤ : ennreal) ≠ n := with_top.top_ne_nat n
id                                 └─┘        └─────┘       └─────────────────┘ 
src                                └─┘        └─────┘        └─────────────────┘
typ                                └─┘        └─────┘       └─────────────────┘ 
doc    └──┘                                    └─────┘
226  
227  lemma le_coe_iff : a ≤ ↑r ↔ (∃p:nnreal, a = p ∧ p ≤ r) := with_top.le_coe_iff r a
id                             └────┘            └─────────────────┘  
src                              └────┘                └─────────────────┘
typ                            └────┘            └─────────────────┘  
doc                                  └────┘
228  lemma coe_le_iff : ↑r ≤ a ↔ (∀p:nnreal, a = p → r ≤ p) := with_top.coe_le_iff r a
id                              └────┘              └─────────────────┘  
src                               └────┘                  └─────────────────┘
typ                             └────┘              └─────────────────┘  
doc                                  └────┘
229  
230  lemma lt_iff_exists_coe : a < b ↔ (∃p:nnreal, a = p ∧ ↑p < b) := with_top.lt_iff_exists_coe a b
id                                    └────┘            └────────────────────────┘  
src                                     └────┘                └────────────────────────┘
typ                                   └────┘            └────────────────────────┘  
doc                                        └────┘
231  
232  @[simp] lemma max_eq_zero_iff : max a b = 0 ↔ a = 0 ∧ b = 0 :=
id                                   └─┘             
src                                  └─┘                 
typ                                  └─┘             
doc    └──┘
233  by simp only [le_zero_iff_eq.symm, max_le_iff]
id                                      └────────┘
src     └─────────┘                   └┘└────────┘└─
typ     └─────────┘└─────────────────┘└┘└────────┘└─
doc     └─────────┘                   └┘          └─
txt     └─────────┘                   └┘          └─
par     └─────────┘                   └┘          └─
pid         └──┘└┘                   └┘          
st     └────────────────────────────────────────────
234  
src  
typ  
doc  
txt  
par  
pid  
st   
235  @[simp] lemma max_zero_left : max 0 a = a := max_eq_right (zero_le a)
id                                 └─┘         └──────────┘  └─────┘ 
src                                └─┘           └──────────┘  └─────┘
typ                                └─┘         └──────────┘  └─────┘ 
doc    └──┘
236  @[simp] lemma max_zero_right : max a 0 = a := max_eq_left (zero_le a)
id                                  └─┘         └─────────┘  └─────┘ 
src                                 └─┘           └─────────┘  └─────┘
typ                                 └─┘         └─────────┘  └─────┘ 
doc    └──┘
237  
238  -- TODO: why this is not a `rfl`? There is some hidden diamond here.
239  @[simp] lemma sup_eq_max : a ⊔ b = max a b :=
id                                  └─┘  
src                                   └─┘
typ                                 └─┘  
doc    └──┘
240  eq_of_forall_ge_iff $ λ c, sup_le_iff.trans max_le_iff.symm
id   └─────────────────┘       └────────┘└────┘ └────────┘└───┘
src  └─────────────────┘        └────────┘└────┘ └────────┘└───┘
typ  └─────────────────┘       └────────┘└────┘ └────────┘└───┘
241  
242  protected lemma pow_pos : 0 < a → ∀ n : ℕ, 0 < a^n :=
id                                              
src                                               
typ                                             
243    canonically_ordered_semiring.pow_pos
id     └──────────────────────────────────┘
src    └──────────────────────────────────┘
typ    └──────────────────────────────────┘
244  
245  protected lemma pow_ne_zero : a ≠ 0 → ∀ n : ℕ, a^n ≠ 0 :=
id                                                
src                                                  
typ                                               
246  by simpa only [zero_lt_iff_ne_zero] using ennreal.pow_pos
id                  └─────────────────┘        └─────────────┘
src     └──────────┘└─────────────────┘└──────┘└─────────────┘
typ     └──────────┘└─────────────────┘└──────┘└─────────────┘
doc     └──────────┘                   └──────┘               
txt     └──────────┘                   └──────┘               
par     └──────────┘                   └──────┘               
pid          └──┘└┘                   └────┘               
st     └───────────────────────────────────────────────────────
247  
src  
typ  
doc  
txt  
par  
pid  
st   
248  @[simp] lemma not_lt_zero : ¬ a < 0 := by simp
id                                 
src                                          └────
typ                                         └────
doc    └──┘                                    └────
txt                                            └────
par                                            └────
pid                                                
st                                            └─────
249  
src  
typ  
doc  
txt  
par  
pid  
st   
250  lemma add_lt_add_iff_left : a < ⊤ → (a + c < a + b ↔ c < b) :=
id                                               
src                                                   
typ                                              
251  with_top.add_lt_add_iff_left
id   └──────────────────────────┘
src  └──────────────────────────┘
typ  └──────────────────────────┘
252  
253  lemma add_lt_add_iff_right : a < ⊤ → (c + a < b + a ↔ c < b) :=
id                                                
src                                                    
typ                                               
254  with_top.add_lt_add_iff_right
id   └───────────────────────────┘
src  └───────────────────────────┘
typ  └───────────────────────────┘
255  
256  lemma lt_add_right (ha : a < ⊤) (hb : 0 < b) : a < a + b :=
id                                                 
src                                                   
typ                                                
257  by rwa [← add_lt_add_iff_left ha, add_zero] at hb
id             └─────────────────┘ └┘  └──────┘
src     └─────┘└─────────────────┘  └┘└──────┘└───────
typ     └─────┘└─────────────────┘└┘└┘└──────┘└───────
doc     └─────┘                     └┘        └───────
txt     └─────┘                     └┘        └───────
par     └─────┘                     └┘        └───────
pid        └──┘                     └┘        └────┘
st     └────────────────────────────┘└────────┘└──────
258  
src  
typ  
doc  
txt  
par  
pid  
st   
259  lemma le_of_forall_epsilon_le : ∀{a b : ennreal}, (∀ε:nnreal, 0 < ε → b < ∞ → a ≤ b + ε) → a ≤ b
id                                          └─────┘      └────┘                       
src                                          └─────┘       └────┘                            
typ                                         └─────┘      └────┘                       
doc                                          └─────┘       └────┘              
260  | a    none     h := le_top
id          └──┘          └────┘
src         └──┘          └────┘
typ         └──┘          └────┘
261  | none (some a) h :=
id     └──┘  └──┘   
src    └──┘  └──┘
typ    └──┘  └──┘   
262    have (⊤:ennreal) ≤ ↑a + ↑(1:nnreal), from h 1 zero_lt_one coe_lt_top,
id            └─────┘         └────┘            └─────────┘ └────────┘
src           └─────┘         └────┘            └─────────┘ └────────┘
typ           └─────┘         └────┘            └─────────┘ └────────┘
doc            └─────┘             └────┘
263    by rw [← coe_add] at this; exact (not_top_le_coe this).elim
id              └─────┘                  └────────────┘ └──┘
src       └────┘└─────┘└───────┘  └────┘ └────────────┘    └─────┘
typ       └────┘└─────┘└───────┘  └────┘ └────────────┘└──┘└─────┘
doc       └────┘       └───────┘  └────┘                   └─────┘
txt       └────┘       └───────┘  └────┘                   └─────┘
par       └────┘       └───────┘  └────┘                   └─────┘
pid         └──┘       └──────┘                          └───┘└┘
st       └────────────┘└─────────────────────────────────────────┘
264  | (some a) (some b) h :=
id               └──┘
src              └──┘
typ              └──┘
265      by simp only [none_eq_top, some_eq_coe, coe_add.symm, coe_le_coe, coe_lt_top, true_implies_iff] at *;
id                     └─────────┘  └─────────┘                └────────┘  └────────┘  └──────────────┘
src         └─────────┘└─────────┘└┘└─────────┘└┘            └┘└────────┘└┘└────────┘└┘└──────────────┘└────┘
typ         └─────────┘└─────────┘└┘└─────────┘└┘└──────────┘└┘└────────┘└┘└────────┘└┘└──────────────┘└────┘
doc         └─────────┘           └┘           └┘            └┘          └┘          └┘                └────┘
txt         └─────────┘           └┘           └┘            └┘          └┘          └┘                └────┘
par         └─────────┘           └┘           └┘            └┘          └┘          └┘                └────┘
pid             └──┘└┘           └┘           └┘            └┘          └┘          └┘                └──┘
st         └───────────────────────────────────────────────────────────────────────────────────────────────────
266        exact nnreal.le_of_forall_epsilon_le h
id               └────────────────────────────┘ 
src        └────┘└────────────────────────────┘ 
typ        └────┘└────────────────────────────┘
doc        └────┘                               
txt        └────┘                               
par        └────┘                               
pid                                            
st   ─────────────────────────────────────────────
267  
src  
typ  
doc  
txt  
par  
pid  
st   
268  lemma lt_iff_exists_rat_btwn :
269    a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < nnreal.of_real q ∧ (nnreal.of_real q:ennreal) < b) :=
id                    └────────────┘    └────────────┘  └─────┘   
src                       └────────────┘     └────────────┘   └─────┘  
typ                   └────────────┘    └────────────┘  └─────┘   
doc                                                                   └─────┘
270  ⟨λ h,
id      
typ     
271    begin
st     └─────
272      rcases lt_iff_exists_coe.1 h with ⟨p, rfl, _⟩,
id              └───────────────┘   
src      └─────┘└───────────────┘└─┘ └───────────────┘
typ      └─────┘└───────────────┘└─┘└───────────────┘
doc      └─────┘                 └─┘ └───────────────┘
txt      └─────┘                 └─┘ └───────────────┘
par      └─────┘                 └─┘ └───────────────┘
pid                             └─┘ └───────────────┘
st   ────────────────────────────────────────────────┘└─
273      rcases dense h with ⟨c, pc, cb⟩,
id              └───┘ 
src      └─────┘└───┘ └───────────────┘
typ      └─────┘└───┘└───────────────┘
doc      └─────┘      └───────────────┘
txt      └─────┘      └───────────────┘
par      └─────┘      └───────────────┘
pid                  └───────────────┘
st   ──────────────────────────────────┘└─
274      rcases lt_iff_exists_coe.1 cb with ⟨r, rfl, _⟩,
id              └───────────────┘   └┘
src      └─────┘└───────────────┘└─┘  └───────────────┘
typ      └─────┘└───────────────┘└─┘└┘└───────────────┘
doc      └─────┘                 └─┘  └───────────────┘
txt      └─────┘                 └─┘  └───────────────┘
par      └─────┘                 └─┘  └───────────────┘
pid                             └─┘  └───────────────┘
st   ─────────────────────────────────────────────────┘└─
275      rcases (nnreal.lt_iff_exists_rat_btwn _ _).1 (coe_lt_coe.1 pc) with ⟨q, hq0, pq, qr⟩,
id               └───────────────────────────┘         └────────┘   └┘
src      └─────┘ └───────────────────────────┘└──────┘ └────────┘└─┘  └─────────────────────┘
typ      └─────┘ └───────────────────────────┘└──────┘ └────────┘└─┘└┘└─────────────────────┘
doc      └─────┘                              └──────┘           └─┘  └─────────────────────┘
txt      └─────┘                              └──────┘           └─┘  └─────────────────────┘
par      └─────┘                              └──────┘           └─┘  └─────────────────────┘
pid                                          └──────┘           └─┘  └─────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
276      exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩
id                └─┘               └┘  └──────┘  └────────┘   └┘  └┘
src      └────┘  └┘   └┘          └─┘  └┘└──────┘ └────────┘└─┘  └┘  └─
typ      └────┘ └┘└─┘└┘          └─┘└┘└┘└──────┘ └────────┘└─┘└┘└┘└┘└─
doc      └────┘  └┘   └┘          └─┘  └┘                   └─┘  └┘  └─
txt      └────┘  └┘   └┘          └─┘  └┘                   └─┘  └┘  └─
par      └────┘  └┘   └┘          └─┘  └┘                   └─┘  └┘  └─
pid             └┘   └┘          └─┘  └┘                   └─┘  └┘  
st   ───────────────────────────────────────────────────────────────────
277    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
278  λ ⟨q, q0, qa, qb⟩, lt_trans qa qb⟩
id            └┘  └┘   └──────┘
src                     └──────┘
typ           └┘  └┘   └──────┘
279  
280  lemma lt_iff_exists_real_btwn :
281    a < b ↔ (∃r:ℝ, 0 ≤ r ∧ a < ennreal.of_real r ∧ (ennreal.of_real r:ennreal) < b) :=
id                    └─────────────┘    └─────────────┘  └─────┘   
src                       └─────────────┘     └─────────────┘   └─────┘  
typ                   └─────────────┘    └─────────────┘  └─────┘   
doc                               └─────────────┘      └─────────────┘   └─────┘
282  ⟨λ h, let ⟨q, q0, aq, qb⟩ := ennreal.lt_iff_exists_rat_btwn.1 h in
id        └─┘    └┘  └┘  └┘     └────────────────────────────┘  
src                               └────────────────────────────┘
typ       └─┘    └┘  └┘  └┘     └────────────────────────────┘  
283    ⟨q, rat.cast_nonneg.2 q0, aq, qb⟩,
id         └─────────────┘
src        └─────────────┘
typ        └─────────────┘
284  λ ⟨q, q0, qa, qb⟩, lt_trans qa qb⟩
id            └┘  └┘   └──────┘
src                     └──────┘
typ           └┘  └┘   └──────┘
285  
286  lemma coe_nat_lt_coe {n : ℕ} : (n : ennreal) < r ↔ ↑n < r := ennreal.coe_nat n ▸ coe_lt_coe
id                                     └─────┘           └─────────────┘   └────────┘
src                                     └─────┘              └─────────────┘    └────────┘
typ                                    └─────┘           └─────────────┘   └────────┘
doc                                      └─────┘
287  lemma coe_lt_coe_nat {n : ℕ} : (r : ennreal) < n ↔ r < n := ennreal.coe_nat n ▸ coe_lt_coe
id                                     └─────┘           └─────────────┘   └────────┘
src                                     └─────┘              └─────────────┘    └────────┘
typ                                    └─────┘           └─────────────┘   └────────┘
doc                                      └─────┘
288  @[elim_cast] lemma coe_nat_lt_coe_nat {m n : ℕ} : (m : ennreal) < n ↔ m < n :=
id                                                        └─────┘       
src                                                        └─────┘        
typ                                                       └─────┘       
doc    └───────┘                                            └─────┘
289  ennreal.coe_nat n ▸ coe_nat_lt_coe.trans nat.cast_lt
id   └─────────────┘   └────────────┘└────┘ └─────────┘
src  └─────────────┘    └────────────┘└────┘ └─────────┘
typ  └─────────────┘   └────────────┘└────┘ └─────────┘
290  lemma coe_nat_ne_top {n : ℕ} : (n : ennreal) ≠ ∞ := ennreal.coe_nat n ▸ coe_ne_top
id                                     └─────┘       └─────────────┘   └────────┘
src                                     └─────┘       └─────────────┘    └────────┘
typ                                    └─────┘       └─────────────┘   └────────┘
doc                                      └─────┘    
291  lemma coe_nat_mono : strict_mono (coe : ℕ → ennreal) := λ _ _, coe_nat_lt_coe_nat.2
id                        └─────────┘  └─┘      └─────┘          └────────────────┘
src                       └─────────┘  └─┘      └─────┘            └────────────────┘
typ                       └─────────┘  └─┘      └─────┘          └────────────────┘
doc                       └─────────┘            └─────┘
292  @[elim_cast] lemma coe_nat_le_coe_nat {m n : ℕ} : (m : ennreal) ≤ n ↔ m ≤ n :=
id                                                        └─────┘       
src                                                        └─────┘        
typ                                                       └─────┘       
doc    └───────┘                                            └─────┘
293  coe_nat_mono.le_iff_le
id   └──────────┘└────────┘
src  └──────────┘└────────┘
typ  └──────────┘└────────┘
294  
295  instance : char_zero ennreal := ⟨coe_nat_mono.injective⟩
id              └───────┘ └─────┘     └──────────┘└────────┘
src             └───────┘ └─────┘     └──────────┘└────────┘
typ             └───────┘ └─────┘     └──────────┘└────────┘
doc             └───────┘ └─────┘
296  
297  protected lemma exists_nat_gt {r : ennreal} (h : r ≠ ⊤) : ∃n:ℕ, r < n :=
id                                      └─────┘                  
src                                     └─────┘                   
typ                                     └─────┘                  
doc                                     └─────┘
298  begin
st   └─────
299    rcases lt_iff_exists_coe.1 (lt_top_iff_ne_top.2 h) with ⟨r, rfl, hb⟩,
id            └───────────────┘    └───────────────┘   
src    └─────┘└───────────────┘└─┘ └───────────────┘└─┘ └─────────────────┘
typ    └─────┘└───────────────┘└─┘ └───────────────┘└─┘└─────────────────┘
doc    └─────┘                 └─┘                  └─┘ └─────────────────┘
txt    └─────┘                 └─┘                  └─┘ └─────────────────┘
par    └─────┘                 └─┘                  └─┘ └─────────────────┘
pid                           └─┘                  └─┘ └─────────────────┘
st   ─────────────────────────────────────────────────────────────────────┘└─
300    rcases exists_nat_gt r with ⟨n, hn⟩,
id            └───────────┘ 
src    └─────┘└───────────┘ └───────────┘
typ    └─────┘└───────────┘└───────────┘
doc    └─────┘              └───────────┘
txt    └─────┘              └───────────┘
par    └─────┘              └───────────┘
pid                        └───────────┘
st   ────────────────────────────────────┘└─
301    exact ⟨n, coe_lt_coe_nat.2 hn⟩,
id              └────────────┘   └┘
src    └────┘  └┘└────────────┘└─┘  
typ    └────┘ └┘└────────────┘└─┘└┘
doc    └────┘  └┘              └─┘  
txt    └────┘  └┘              └─┘  
par    └────┘  └┘              └─┘  
pid           └┘              └─┘  
st   ───────────────────────────────┘└─
302  end
st   ──┘
303  
304  lemma add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d :=
id                                                
src                                                     
typ                                               
305  begin
st   └─────
306    rcases dense ac with ⟨a', aa', a'c⟩,
id            └───┘ └┘
src    └─────┘└───┘  └──────────────────┘
typ    └─────┘└───┘└┘└──────────────────┘
doc    └─────┘       └──────────────────┘
txt    └─────┘       └──────────────────┘
par    └─────┘       └──────────────────┘
pid                 └──────────────────┘
st   ────────────────────────────────────┘└─
307    rcases lt_iff_exists_coe.1 aa' with ⟨aR, rfl, _⟩,
id            └───────────────┘   └─┘
src    └─────┘└───────────────┘└─┘   └────────────────┘
typ    └─────┘└───────────────┘└─┘└─┘└────────────────┘
doc    └─────┘                 └─┘   └────────────────┘
txt    └─────┘                 └─┘   └────────────────┘
par    └─────┘                 └─┘   └────────────────┘
pid                           └─┘   └────────────────┘
st   ─────────────────────────────────────────────────┘└─
308    rcases lt_iff_exists_coe.1 a'c with ⟨a'R, rfl, _⟩,
id            └───────────────┘   └─┘
src    └─────┘└───────────────┘└─┘   └─────────────────┘
typ    └─────┘└───────────────┘└─┘└─┘└─────────────────┘
doc    └─────┘                 └─┘   └─────────────────┘
txt    └─────┘                 └─┘   └─────────────────┘
par    └─────┘                 └─┘   └─────────────────┘
pid                           └─┘   └─────────────────┘
st   ──────────────────────────────────────────────────┘└─
309    rcases dense bd with ⟨b', bb', b'd⟩,
id            └───┘ └┘
src    └─────┘└───┘  └──────────────────┘
typ    └─────┘└───┘└┘└──────────────────┘
doc    └─────┘       └──────────────────┘
txt    └─────┘       └──────────────────┘
par    └─────┘       └──────────────────┘
pid                 └──────────────────┘
st   ────────────────────────────────────┘└─
310    rcases lt_iff_exists_coe.1 bb' with ⟨bR, rfl, _⟩,
id            └───────────────┘   └─┘
src    └─────┘└───────────────┘└─┘   └────────────────┘
typ    └─────┘└───────────────┘└─┘└─┘└────────────────┘
doc    └─────┘                 └─┘   └────────────────┘
txt    └─────┘                 └─┘   └────────────────┘
par    └─────┘                 └─┘   └────────────────┘
pid                           └─┘   └────────────────┘
st   ─────────────────────────────────────────────────┘└─
311    rcases lt_iff_exists_coe.1 b'd with ⟨b'R, rfl, _⟩,
id            └───────────────┘   └─┘
src    └─────┘└───────────────┘└─┘   └─────────────────┘
typ    └─────┘└───────────────┘└─┘└─┘└─────────────────┘
doc    └─────┘                 └─┘   └─────────────────┘
txt    └─────┘                 └─┘   └─────────────────┘
par    └─────┘                 └─┘   └─────────────────┘
pid                           └─┘   └─────────────────┘
st   ──────────────────────────────────────────────────┘└─
312    have I : ↑aR + ↑bR < ↑a'R + ↑b'R :=
id              └┘   └┘   └─┘    └─┘
src    └───────┘              └───
typ    └───────┘└┘ └┘ └─┘  └─┘└───
doc    └───────┘                 └───
txt    └───────┘                 └───
par    └───────┘                 └───
pid    └────┘└─┘                 └───
st   ──────────────────────────────────────
313    begin
src  ─┘     
typ  ─┘     
doc  ─┘     
txt  ─┘     
par  ─┘     
pid  ─┘     
st   ─┘└─────
314      rw [← coe_add, ← coe_add, coe_lt_coe],
id             └─────┘    └─────┘  └────────┘
src  ───┘└────┘└─────┘└──┘└─────┘└┘└────────┘└─
typ  ───┘└────┘└─────┘└──┘└─────┘└┘└────────┘└─
doc  ───┘└────┘       └──┘       └┘          └─
txt  ───┘└────┘       └──┘       └┘          └─
par  ───┘└────┘       └──┘       └┘          └─
pid  ─────────┘       └──┘       └┘          └──
st   ────────────────┘└─────────┘└──────────┘└──
315      apply add_lt_add (coe_lt_coe.1 aa') (coe_lt_coe.1 bb')
id             └────────┘               └─┘   └────────┘   └─┘
src  ───┘└────┘└────────┘           └─┘   └┘ └────────┘└─┘   └─
typ  ───┘└────┘└────────┘           └─┘└─┘└┘ └────────┘└─┘└─┘└─
doc  ───┘└────┘                     └─┘   └┘           └─┘   └─
txt  ───┘└────┘                     └─┘   └┘           └─┘   └─
par  ───┘└────┘                     └─┘   └┘           └─┘   └─
pid  ─────────┘                     └─┘   └┘           └─┘   └─
st   ───────────────────────────────────────────────────────────
316    end,
src  ─┘└─┘
typ  ─┘└─┘
doc  ─┘└─┘
txt  ─┘└─┘
par  ─┘└─┘
pid  ────┘
st   ─┘└─┘└─
317    have J : ↑a'R + ↑b'R ≤ c + d := add_le_add' (le_of_lt a'c) (le_of_lt b'd),
id               └─┘    └─┘         └─────────┘           └─┘   └──────┘ └─┘
src    └───────┘            └──┘└─────────┘            └┘ └──────┘   
typ    └───────┘ └─┘  └─┘ └──┘└─────────┘         └─┘└┘ └──────┘└─┘
doc    └───────┘             └──┘                       └┘            
txt    └───────┘             └──┘                       └┘            
par    └───────┘             └──┘                       └┘            
pid    └────┘└─┘             └──┘                       └┘            
st   ──────────────────────────────────────────────────────────────────────────┘└─
318    apply lt_of_lt_of_le I J
id           └────────────┘  
src    └────┘└────────────┘  
typ    └────┘└────────────┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ──────────────────────────┘
319  end
st   └─┘
320  
321  @[move_cast] lemma coe_min : ((min r p:nnreal):ennreal) = min r p :=
id                                  └─┘   └────┘  └─────┘   └─┘  
src                                 └─┘     └────┘  └─────┘   └─┘
typ                                 └─┘   └────┘  └─────┘   └─┘  
doc    └───────┘                            └────┘  └─────┘
322  coe_mono.map_min
id   └──────┘└──────┘
src  └──────┘└──────┘
typ  └──────┘└──────┘
323  
324  @[move_cast] lemma coe_max : ((max r p:nnreal):ennreal) = max r p :=
id                                  └─┘   └────┘  └─────┘   └─┘  
src                                 └─┘     └────┘  └─────┘   └─┘
typ                                 └─┘   └────┘  └─────┘   └─┘  
doc    └───────┘                            └────┘  └─────┘
325  coe_mono.map_max
id   └──────┘└──────┘
src  └──────┘└──────┘
typ  └──────┘└──────┘
326  
327  end order
328  
329  section complete_lattice
330  
331  lemma coe_Sup {s : set nnreal} : bdd_above s → (↑(Sup s) : ennreal) = (⨆a∈s, ↑a) := with_top.coe_Sup
id                      └─┘ └────┘    └───────┘      └─┘     └─────┘           └──────────────┘
src                     └─┘ └────┘    └───────┘       └─┘      └─────┘              └──────────────┘
typ                     └─┘ └────┘    └───────┘      └─┘     └─────┘           └──────────────┘
doc                         └────┘    └───────┘        └─┘      └─────┘        
332  lemma coe_Inf {s : set nnreal} : s.nonempty → (↑(Inf s) : ennreal) = (⨅a∈s, ↑a) := with_top.coe_Inf
id                      └─┘ └────┘    └───────┘     └─┘     └─────┘           └──────────────┘
src                     └─┘ └────┘     └───────┘     └─┘      └─────┘              └──────────────┘
typ                     └─┘ └────┘    └───────┘     └─┘     └─────┘           └──────────────┘
doc                         └────┘     └───────┘      └─┘      └─────┘        
333  
334  @[simp] lemma top_mem_upper_bounds {s : set ennreal} : ∞ ∈ upper_bounds s :=
id                                           └─┘ └─────┘      └──────────┘ 
src                                          └─┘ └─────┘      └──────────┘
typ                                          └─┘ └─────┘      └──────────┘ 
doc    └──┘                                      └─────┘       └──────────┘
335  assume x hx, le_top
id           └┘  └────┘
src               └────┘
typ          └┘  └────┘
336  
337  lemma coe_mem_upper_bounds {s : set nnreal} :
id                                   └─┘ └────┘
src                                  └─┘ └────┘
typ                                  └─┘ └────┘
doc                                      └────┘
338    ↑r ∈ upper_bounds ((coe : nnreal → ennreal) '' s) ↔ r ∈ upper_bounds s :=
id       └──────────┘   └─┘   └────┘   └─────┘  └┘      └──────────┘ 
src       └──────────┘   └─┘   └────┘   └─────┘  └┘        └──────────┘
typ      └──────────┘   └─┘   └────┘   └─────┘  └┘      └──────────┘ 
doc         └──────────┘         └────┘   └─────┘              └──────────┘
339  by simp [upper_bounds, ball_image_iff, -mem_image, *] {contextual := tt}
id            └──────────┘  └────────────┘                                └┘
src     └────┘└──────────┘└┘└────────────┘└───────────────┘ └────────────┘└┘└─
typ     └────┘└──────────┘└┘└────────────┘└───────────────┘ └────────────┘└┘└─
doc     └────┘└──────────┘└┘              └───────────────┘ └────────────┘  └─
txt     └────┘            └┘              └───────────────┘ └────────────┘  └─
par     └────┘            └┘              └───────────────┘ └────────────┘  └─
pid                     └┘              └──────────────┘ └────────────┘  
st     └──────────────────────────────────────────────────────────────────────
340  
src  
typ  
doc  
txt  
par  
pid  
st   
341  lemma infi_ennreal {α : Type*} [complete_lattice α] {f : ennreal → α} :
id                                   └──────────────┘        └─────┘   
src                                  └──────────────┘         └─────┘
typ                                  └──────────────┘        └─────┘   
doc                                  └──────────────┘         └─────┘
342    (⨅n, f n) = (⨅n:nnreal, f n) ⊓ f ⊤ :=
id              └────┘      
src                └────┘         
typ             └────┘      
doc                 └────┘
343  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
344    (le_inf (le_infi $ assume i, infi_le _ _) (infi_le _ _))
id      └────┘  └─────┘            └─────┘       └─────┘
src     └────┘  └─────┘             └─────┘       └─────┘
typ     └────┘  └─────┘            └─────┘       └─────┘
345    (le_infi $ forall_ennreal.2 ⟨assume r, inf_le_left_of_le $ infi_le _ _, inf_le_right⟩)
id      └─────┘   └────────────┘            └───────────────┘   └─────┘      └──────────┘
src     └─────┘   └────────────┘             └───────────────┘   └─────┘      └──────────┘
typ     └─────┘   └────────────┘            └───────────────┘   └─────┘      └──────────┘
346  
347  end complete_lattice
348  
349  section mul
350  
351  lemma mul_le_mul : a ≤ b → c ≤ d → a * c ≤ b * d :=
id                                      
src                                           
typ                                     
352  canonically_ordered_semiring.mul_le_mul
id   └─────────────────────────────────────┘
src  └─────────────────────────────────────┘
typ  └─────────────────────────────────────┘
353  
354  lemma mul_left_mono : monotone ((*) a) := λ b c, mul_le_mul (le_refl a)
id                         └──────┘               └────────┘  └─────┘ 
src                        └──────┘                  └────────┘  └─────┘
typ                        └──────┘               └────────┘  └─────┘ 
doc                        └──────┘
355  
356  lemma mul_right_mono : monotone (λ x, x * a) := λ b c h, mul_le_mul h (le_refl a)
id                          └──────┘                   └────────┘   └─────┘ 
src                         └──────┘                         └────────┘    └─────┘
typ                         └──────┘                   └────────┘   └─────┘ 
doc                         └──────┘
357  
358  lemma max_mul : max a b * c = max (a * c) (b * c) :=
id                   └─┘      └─┘         
src                  └─┘         └─┘           
typ                  └─┘      └─┘         
359  mul_right_mono.map_max
id   └────────────┘└──────┘
src  └────────────┘└──────┘
typ  └────────────┘└──────┘
360  
361  lemma mul_max : a * max b c = max (a * b) (a * c) :=
id                     └─┘    └─┘         
src                     └─┘      └─┘           
typ                    └─┘    └─┘         
362  mul_left_mono.map_max
id   └───────────┘└──────┘
src  └───────────┘└──────┘
typ  └───────────┘└──────┘
363  
364  lemma mul_eq_mul_left : a ≠ 0 → a ≠ ⊤ → (a * b = a * c ↔ b = c) :=
id                                                 
src                                                      
typ                                                
365  begin
st   └─────
366    cases a; cases b; cases c;
id                           
src    └────┘   └────┘   └────┘
typ    └────┘  └────┘  └────┘
doc    └────┘   └────┘   └────┘
txt    └────┘   └────┘   └────┘
par    └────┘   └────┘   └────┘
pid                         
st   ─────────────────────────────
367      simp [none_eq_top, some_eq_coe, mul_top, top_mul, -coe_mul, coe_mul.symm,
id             └─────────┘  └─────────┘  └─────┘  └─────┘
src      └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└──────────┘            └─
typ      └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└──────────┘└──────────┘└─
doc      └────┘           └┘           └┘       └┘       └──────────┘            └─
txt      └────┘           └┘           └┘       └┘       └──────────┘            └─
par      └────┘           └┘           └┘       └┘       └──────────┘            └─
pid                     └┘           └┘       └┘       └──────────┘            └─
st   ──────────────────────────────────────────────────────────────────────────────
368        nnreal.mul_eq_mul_left] {contextual := tt},
id         └────────────────────┘                 └┘
src  ─────┘└────────────────────┘└┘ └────────────┘└┘
typ  ─────┘└────────────────────┘└┘ └────────────┘└┘
doc  ─────┘                      └┘ └────────────┘  
txt  ─────┘                      └┘ └────────────┘  
par  ─────┘                      └┘ └────────────┘  
pid  ─────┘                       └────────────┘  
st   ───────────────────────────────────────────────┘└─
369  end
st   ──┘
370  
371  lemma mul_eq_mul_right : c ≠ 0 → c ≠ ∞ → (a * c = b * c ↔ a = b) :=
id                                                  
src                                                       
typ                                                 
doc                                       
372  mul_comm c a ▸ mul_comm c b ▸ mul_eq_mul_left
id   └──────┘    └──────┘    └─────────────┘
src  └──────┘      └──────┘      └─────────────┘
typ  └──────┘    └──────┘    └─────────────┘
373  
374  lemma mul_le_mul_left : a ≠ 0 → a ≠ ⊤ → (a * b ≤ a * c ↔ b ≤ c) :=
id                                                 
src                                                      
typ                                                
375  begin
st   └─────
376    cases a; cases b; cases c;
id                           
src    └────┘   └────┘   └────┘
typ    └────┘  └────┘  └────┘
doc    └────┘   └────┘   └────┘
txt    └────┘   └────┘   └────┘
par    └────┘   └────┘   └────┘
pid                         
st   ─────────────────────────────
377      simp [none_eq_top, some_eq_coe, mul_top, top_mul, -coe_mul, coe_mul.symm] {contextual := tt},
id             └─────────┘  └─────────┘  └─────┘  └─────┘                                         └┘
src      └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└──────────┘            └┘ └────────────┘└┘
typ      └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└──────────┘└──────────┘└┘ └────────────┘└┘
doc      └────┘           └┘           └┘       └┘       └──────────┘            └┘ └────────────┘  
txt      └────┘           └┘           └┘       └┘       └──────────┘            └┘ └────────────┘  
par      └────┘           └┘           └┘       └┘       └──────────┘            └┘ └────────────┘  
pid                     └┘           └┘       └┘       └──────────┘             └────────────┘  
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
378    assume h, exact mul_le_mul_left (zero_lt_iff_ne_zero.2 h)
id                     └─────────────┘  └─────────────────┘   
src    └──────┘  └────┘└─────────────┘ └─────────────────┘└─┘ └┘
typ    └──────┘  └────┘└─────────────┘ └─────────────────┘└─┘└┘
doc    └──────┘  └────┘                                   └─┘ └┘
txt    └──────┘  └────┘                                   └─┘ └┘
par    └──────┘  └────┘                                   └─┘ └┘
pid    └──────┘                                          └─┘ 
st   ─────────┘└────────────────────────────────────────────────┘
379  end
st   └─┘
380  
381  lemma mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b) :=
id                                                  
src                                                       
typ                                                 
doc                                       
382  mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left
id   └──────┘    └──────┘    └─────────────┘
src  └──────┘      └──────┘      └─────────────┘
typ  └──────┘    └──────┘    └─────────────┘
383  
384  lemma mul_lt_mul_left : a ≠ 0 → a ≠ ⊤ → (a * b < a * c ↔ b < c) :=
id                                                 
src                                                      
typ                                                
385  λ h0 ht, by simp only [mul_le_mul_left h0 ht, lt_iff_le_not_le]
id     └┘ └┘                └─────────────┘ └┘ └┘  └──────────────┘
src              └─────────┘└─────────────┘    └┘└──────────────┘└─
typ    └┘ └┘     └─────────┘└─────────────┘└┘└┘└┘└──────────────┘└─
doc              └─────────┘                   └┘                └─
txt              └─────────┘                   └┘                └─
par              └─────────┘                   └┘                └─
pid                  └──┘└┘                   └┘                
st              └────────────────────────────────────────────────────
386  
src  
typ  
doc  
txt  
par  
pid  
st   
387  lemma mul_lt_mul_right : c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b) :=
id                                                  
src                                                       
typ                                                 
doc                                       
388  mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_left
id   └──────┘    └──────┘    └─────────────┘
src  └──────┘      └──────┘      └─────────────┘
typ  └──────┘    └──────┘    └─────────────┘
389  
390  lemma mul_eq_zero {a b : ennreal} : a * b = 0 ↔ a = 0 ∨ b = 0 :=
id                            └─────┘                 
src                           └─────┘                     
typ                           └─────┘                 
doc                           └─────┘
391  canonically_ordered_comm_semiring.mul_eq_zero_iff _ _
id   └───────────────────────────────────────────────┘
src  └───────────────────────────────────────────────┘
typ  └───────────────────────────────────────────────┘
392  
393  end mul
394  
395  section sub
396  instance : has_sub ennreal := ⟨λa b, Inf {d | a ≤ d + b}⟩
id              └─────┘ └─────┘         └─┘        
src             └─────┘ └─────┘           └─┘          
typ             └─────┘ └─────┘         └─┘        
doc                     └─────┘           └─┘
397  
398  @[move_cast] lemma coe_sub : ↑(p - r) = (↑p:ennreal) - r :=
id                                        └─────┘   
src                                          └─────┘  
typ                                       └─────┘   
doc    └───────┘                                 └─────┘
399  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
400    (le_Inf $ assume b (hb : ↑p ≤ b + r), coe_le_iff.2 $
id      └────┘                        └────────┘
src     └────┘                            └────────┘
typ     └────┘                        └────────┘
401      by rintros d rfl; rwa [← coe_add, coe_le_coe, ← nnreal.sub_le_iff_le_add] at hb)
id                                └─────┘  └────────┘    └──────────────────────┘
src         └───────────┘  └─────┘└─────┘└┘└────────┘└──┘└──────────────────────┘└─────┘
typ         └───────────┘  └─────┘└─────┘└┘└────────┘└──┘└──────────────────────┘└─────┘
doc         └───────────┘  └─────┘       └┘          └──┘                        └─────┘
txt         └───────────┘  └─────┘       └┘          └──┘                        └─────┘
par         └───────────┘  └─────┘       └┘          └──┘                        └─────┘
pid                └────┘     └──┘       └┘          └──┘                        └────┘
st         └───────────────────┘└───────┘└──────────┘└──────────────────────────┘└────┘
402    (Inf_le $ show (↑p : ennreal) ≤ ↑(p - r) + ↑r,
id      └────┘            └─────┘         
src     └────┘             └─────┘           
typ     └────┘            └─────┘         
doc                         └─────┘
403      by rw [← coe_add, coe_le_coe, ← nnreal.sub_le_iff_le_add])
id                └─────┘  └────────┘    └──────────────────────┘
src         └────┘└─────┘└┘└────────┘└──┘└──────────────────────┘
typ         └────┘└─────┘└┘└────────┘└──┘└──────────────────────┘
doc         └────┘       └┘          └──┘                        
txt         └────┘       └┘          └──┘                        
par         └────┘       └┘          └──┘                        
pid           └──┘       └┘          └──┘                        
st         └────────────┘└──────────┘└──────────────────────────┘
404  
405  @[simp] lemma top_sub_coe : ∞ - ↑r = ∞ :=
id                                   
src                                   
typ                                  
doc    └──┘                              
406  top_unique $ le_Inf $ by simp [add_eq_top]
id   └────────┘   └────┘            └────────┘
src  └────────┘   └────┘      └────┘└────────┘└─
typ  └────────┘   └────┘      └────┘└────────┘└─
doc                           └────┘          └─
txt                           └────┘          └─
par                           └────┘          └─
pid                                         
st                           └──────────────────
407  
src  
typ  
doc  
txt  
par  
pid  
st   
408  @[simp] lemma sub_eq_zero_of_le (h : a ≤ b) : a - b = 0 :=
id                                                 
src                                                    
typ                                                
doc    └──┘
409  le_antisymm (Inf_le $ le_add_left h) (zero_le _)
id   └─────────┘  └────┘   └─────────┘    └─────┘
src  └─────────┘  └────┘   └─────────┘     └─────┘
typ  └─────────┘  └────┘   └─────────┘    └─────┘
410  
411  @[simp] lemma sub_self : a - a = 0 := sub_eq_zero_of_le $ le_refl _
id                                     └───────────────┘   └─────┘
src                                      └───────────────┘   └─────┘
typ                                    └───────────────┘   └─────┘
doc    └──┘
412  
413  @[simp] lemma zero_sub : 0 - a = 0 :=
id                                
src                                
typ                               
doc    └──┘
414  le_antisymm (Inf_le $ zero_le _) (zero_le _)
id   └─────────┘  └────┘   └─────┘     └─────┘
src  └─────────┘  └────┘   └─────┘     └─────┘
typ  └─────────┘  └────┘   └─────┘     └─────┘
415  
416  @[simp] lemma sub_infty : a - ∞ = 0 :=
id                                
src                                
typ                               
doc    └──┘                        
417  le_antisymm (Inf_le $ by simp) (zero_le _)
id   └─────────┘  └────┘             └─────┘
src  └─────────┘  └────┘      └──┘   └─────┘
typ  └─────────┘  └────┘      └──┘   └─────┘
doc                           └──┘
txt                           └──┘
par                           └──┘
st                           └───┘
418  
419  @[simp] lemma coe_sub_infty : ↑p - ∞ = 0 :=
id                                    
src                                    
typ                                   
doc    └──┘                             
420  le_antisymm (Inf_le $ by simp) (zero_le _)
id   └─────────┘  └────┘             └─────┘
src  └─────────┘  └────┘      └──┘   └─────┘
typ  └─────────┘  └────┘      └──┘   └─────┘
doc                           └──┘
txt                           └──┘
par                           └──┘
st                           └───┘
421  
422  lemma sub_le_sub (h₁ : a ≤ b) (h₂ : d ≤ c) : a - c ≤ b - d :=
id                                                
src                                                     
typ                                               
423  Inf_le_Inf $ assume e (h : b ≤ e + d),
id   └────────┘                    
src  └────────┘                      
typ  └────────┘                    
424    calc a ≤ b : h₁
id                └┘
typ               └┘
425      ... ≤ e + d : h
id                  
src              
typ                 
426      ... ≤ e + c : add_le_add' (le_refl _) h₂
id                  └─────────┘  └─────┘    └┘
src                   └─────────┘  └─────┘
typ                 └─────────┘  └─────┘    └┘
427  
428  @[simp] lemma add_sub_self : ∀{a b : ennreal}, b < ∞ → (a + b) - b = a
id                                       └─────┘                
src                                       └─────┘                   
typ                                      └─────┘                
doc    └──┘                               └─────┘       
429  | a        none     := by simp [none_eq_top]
id              └──┘                 └─────────┘
src             └──┘           └────┘└─────────┘└┘
typ             └──┘           └────┘└─────────┘└┘
doc                            └────┘           └┘
txt                            └────┘           └┘
par                            └────┘           └┘
pid                                           
st                            └──────────────────┘
430  | none     (some b) := by simp [none_eq_top, some_eq_coe]
id     └──┘      └──┘                └─────────┘  └─────────┘
src    └──┘      └──┘          └────┘└─────────┘└┘└─────────┘└┘
typ    └──┘      └──┘          └────┘└─────────┘└┘└─────────┘└┘
doc                            └────┘           └┘           └┘
txt                            └────┘           └┘           └┘
par                            └────┘           └┘           └┘
pid                                           └┘           
st                            └───────────────────────────────┘
431  | (some a) (some b) :=
id               └──┘
src              └──┘
typ              └──┘
432    by simp [some_eq_coe]; rw [← coe_add, ← coe_sub, coe_eq_coe, nnreal.add_sub_cancel]
id              └─────────┘         └─────┘    └─────┘  └────────┘  └───────────────────┘
src       └────┘└─────────┘  └────┘└─────┘└──┘└─────┘└┘└────────┘└┘└───────────────────┘└─
typ       └────┘└─────────┘  └────┘└─────┘└──┘└─────┘└┘└────────┘└┘└───────────────────┘└─
doc       └────┘             └────┘       └──┘       └┘          └┘                     └─
txt       └────┘             └────┘       └──┘       └┘          └┘                     └─
par       └────┘             └────┘       └──┘       └┘          └┘                     └─
pid                          └──┘       └──┘       └┘          └┘                     
st       └───────────────────────┘└───────┘└─────────┘└──────────┘└─────────────────────┘
433  
src  
typ  
doc  
txt  
par  
pid  
st   
434  @[simp] lemma add_sub_self' (h : a < ∞) : (a + b) - a = b :=
id                                                  
src                                                    
typ                                                 
doc    └──┘                               
435  by rw [add_comm, add_sub_self h]
id          └──────┘  └──────────┘ 
src     └──┘└──────┘└┘└──────────┘ └─
typ     └──┘└──────┘└┘└──────────┘└─
doc     └──┘        └┘             └─
txt     └──┘        └┘             └─
par     └──┘        └┘             └─
pid       └┘        └┘             
st     └───────────┘└──────────────┘
436  
src  
typ  
doc  
txt  
par  
pid  
st   
437  lemma add_left_inj (h : a < ∞) : a + b = a + c ↔ b = c :=
id                                           
src                                               
typ                                          
doc                              
438  ⟨λ e, by simpa [h] using congr_arg (λ x, x - a) e, congr_arg _⟩
id                          └───────┘              └───────┘
src           └─────┘ └──────┘└───────┘  └──┘  └┘   └───────┘
typ          └─────┘└──────┘└───────┘  └──┘ └┘  └───────┘
doc           └─────┘ └──────┘           └──┘   └┘
txt           └─────┘ └──────┘           └──┘   └┘
par           └─────┘ └──────┘           └──┘   └┘
pid                 └────┘           └──┘   └┘
st           └───────────────────────────────────────┘
439  
440  lemma add_right_inj (h : a < ∞) : b + a = c + a ↔ b = c :=
id                                            
src                                                
typ                                           
doc                               
441  by rw [add_comm, add_comm c, add_left_inj h]
id          └──────┘  └──────┘   └──────────┘ 
src     └──┘└──────┘└┘└──────┘ └┘└──────────┘ └─
typ     └──┘└──────┘└┘└──────┘└┘└──────────┘└─
doc     └──┘        └┘         └┘             └─
txt     └──┘        └┘         └┘             └─
par     └──┘        └┘         └┘             └─
pid       └┘        └┘         └┘             
st     └───────────┘└──────────┘└──────────────┘
442  
src  
typ  
doc  
txt  
par  
pid  
st   
443  @[simp] lemma sub_add_cancel_of_le : ∀{a b : ennreal}, b ≤ a → (a - b) + b = a :=
id                                                └─────┘                
src                                               └─────┘                    
typ                                               └─────┘                
doc    └──┘                                       └─────┘
444  begin
st   └─────
445    simp [forall_ennreal, le_coe_iff, -add_comm] {contextual := tt},
id           └────────────┘  └────────┘                            └┘
src    └────┘└────────────┘└┘└────────┘└───────────┘ └────────────┘└┘
typ    └────┘└────────────┘└┘└────────┘└───────────┘ └────────────┘└┘
doc    └────┘              └┘          └───────────┘ └────────────┘  
txt    └────┘              └┘          └───────────┘ └────────────┘  
par    └────┘              └┘          └───────────┘ └────────────┘  
pid                      └┘          └──────────┘ └────────────┘  
st   ────────────────────────────────────────────────────────────────┘└─
446    rintros r p x rfl h,
src    └─────────────────┘
typ    └─────────────────┘
doc    └─────────────────┘
txt    └─────────────────┘
par    └─────────────────┘
pid           └──────────┘
st   ────────────────────┘└─
447    rw [← coe_sub, ← coe_add, nnreal.sub_add_cancel_of_le h]
id           └─────┘    └─────┘  └─────────────────────────┘ 
src    └────┘└─────┘└──┘└─────┘└┘└─────────────────────────┘ └┘
typ    └────┘└─────┘└──┘└─────┘└┘└─────────────────────────┘└┘
doc    └────┘       └──┘       └┘                            └┘
txt    └────┘       └──┘       └┘                            └┘
par    └────┘       └──┘       └┘                            └┘
pid      └──┘       └──┘       └┘                            
st   ──────────────┘└─────────┘└─────────────────────────────┘
448  end
st   └─┘
449  
450  @[simp] lemma add_sub_cancel_of_le (h : b ≤ a) : b + (a - b) = a :=
id                                                         
src                                                            
typ                                                        
doc    └──┘
451  by rwa [add_comm, sub_add_cancel_of_le]
id           └──────┘  └──────────────────┘
src     └───┘└──────┘└┘└──────────────────┘└─
typ     └───┘└──────┘└┘└──────────────────┘└─
doc     └───┘        └┘                    └─
txt     └───┘        └┘                    └─
par     └───┘        └┘                    └─
pid        └┘        └┘                    
st     └────────────┘└────────────────────┘
452  
src  
typ  
doc  
txt  
par  
pid  
st   
453  lemma sub_add_self_eq_max : (a - b) + b = max a b :=
id                                       └─┘  
src                                         └─┘
typ                                      └─┘  
454  match le_total a b with
id         └──────┘  
src        └──────┘
typ        └──────┘  
455  | or.inl h := by simp [h, max_eq_right]
id     └────┘                 └──────────┘
src    └────┘         └────┘ └┘└──────────┘└┘
typ    └────┘         └────┘└┘└──────────┘└┘
doc                   └────┘ └┘            └┘
txt                   └────┘ └┘            └┘
par                   └────┘ └┘            └┘
pid                        └┘            
st                   └──────────────────────┘
456  | or.inr h := by simp [h, max_eq_left]
id     └────┘                 └─────────┘
src    └────┘         └────┘ └┘└─────────┘└┘
typ    └────┘         └────┘└┘└─────────┘└┘
doc                   └────┘ └┘           └┘
txt                   └────┘ └┘           └┘
par                   └────┘ └┘           └┘
pid                        └┘           
st                   └─────────────────────┘
457  end
458  
459  lemma le_sub_add_self : a ≤ (a - b) + b :=
id                                   
src                                    
typ                                  
460  by { rw sub_add_self_eq_max, exact le_max_left a b }
id           └─────────────────┘        └─────────┘  
src       └─┘└─────────────────┘  └────┘└─────────┘  
typ       └─┘└─────────────────┘  └────┘└─────────┘
doc       └─┘                     └────┘             
txt       └─┘                     └────┘             
par       └─┘                     └────┘             
pid                                                
st     └───────────────────────┘└──────────────────────┘└┘
461  
462  @[simp] protected lemma sub_le_iff_le_add : a - b ≤ c ↔ a ≤ c + b :=
id                                                         
src                                                            
typ                                                        
doc    └──┘
463  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
464    (assume h : a - b ≤ c,
id                     
src                     
typ                    
465      calc a ≤ (a - b) + b : le_sub_add_self
id                        └─────────────┘
src                           └─────────────┘
typ                       └─────────────┘
466        ... ≤ c + b : add_le_add_right' h)
id                    └───────────────┘ 
src                     └───────────────┘
typ                   └───────────────┘ 
467    (assume h : a ≤ c + b,
id                     
src                     
typ                    
468      calc a - b ≤ (c + b) - b : sub_le_sub h (le_refl _)
id                          └────────┘   └─────┘
src                              └────────┘    └─────┘
typ                         └────────┘   └─────┘
469        ... ≤ c : Inf_le (le_refl (c + b)))
id                  └────┘  └─────┘    
src                  └────┘  └─────┘    
typ                 └────┘  └─────┘    
470  
471  protected lemma sub_le_iff_le_add' : a - b ≤ c ↔ a ≤ b + c :=
id                                                  
src                                                     
typ                                                 
472  add_comm c b ▸ ennreal.sub_le_iff_le_add
id   └──────┘    └───────────────────────┘
src  └──────┘      └───────────────────────┘
typ  └──────┘    └───────────────────────┘
473  
474  lemma sub_eq_of_add_eq : b ≠ ∞ → a + b = c → c - b = a :=
id                                            
src                                                
typ                                           
doc                               
475  λ hb hc, hc ▸ add_sub_self (lt_top_iff_ne_top.2 hb)
id     └┘ └┘  └┘  └──────────┘  └───────────────┘  └┘
src               └──────────┘  └───────────────┘
typ    └┘ └┘  └┘  └──────────┘  └───────────────┘  └┘
476  
477  protected lemma sub_le_of_sub_le (h : a - b ≤ c) : a - c ≤ b :=
id                                                     
src                                                        
typ                                                    
478  ennreal.sub_le_iff_le_add.2 $ by { rw add_comm, exact ennreal.sub_le_iff_le_add.1 h }
id   └───────────────────────┘            └──────┘        └───────────────────────┘   
src  └───────────────────────┘         └─┘└──────┘  └────┘└───────────────────────┘└─┘ 
typ  └───────────────────────┘         └─┘└──────┘  └────┘└───────────────────────┘└─┘
doc                                     └─┘          └────┘                         └─┘ 
txt                                     └─┘          └────┘                         └─┘ 
par                                     └─┘          └────┘                         └─┘ 
pid                                                                               └─┘ 
st                                   └────────────┘└────────────────────────────────────┘└┘
479  
480  protected lemma sub_lt_sub_self : a ≠ ⊤ → a ≠ 0 → 0 < b → a - b < a :=
id                                                          
src                                                             
typ                                                         
481  match a, b with
id           
typ          
482  | none, _ := by { have := none_eq_top, assume h, contradiction }
id     └──┘                    └─────────┘
src    └──┘            └──────┘└─────────┘  └──────┘  └────────────┘
typ    └──┘            └──────┘└─────────┘  └──────┘  └────────────┘
doc                    └──────┘             └──────┘  └────────────┘
txt                    └──────┘             └──────┘  └────────────┘
par                    └──────┘             └──────┘  └────────────┘
pid                    └───┘└─┘             └──────┘               
st                  └────────────────────┘└────────┘└──────────────┘└┘
483  | (some a), none := by {intros, simp only [none_eq_top, sub_infty, zero_lt_iff_ne_zero], assumption}
id      └──┘     └──┘                           └─────────┘  └───────┘  └─────────────────┘
src     └──┘     └──┘        └────┘  └─────────┘└─────────┘└┘└───────┘└┘└─────────────────┘  └────────┘
typ     └──┘     └──┘        └────┘  └─────────┘└─────────┘└┘└───────┘└┘└─────────────────┘  └────────┘
doc                          └────┘  └─────────┘           └┘         └┘                     └────────┘
txt                          └────┘  └─────────┘           └┘         └┘                     └────────┘
par                          └────┘  └─────────┘           └┘         └┘                     └────────┘
pid                                      └──┘└┘           └┘         └┘                   
st                         └──────┘└───────────────────────────────────────────────────────┘└──────────┘└┘
484  | (some a), (some b) :=
id                └──┘
src               └──┘
typ               └──┘
485    begin
st     └─────
486      simp only [some_eq_coe, coe_sub.symm, coe_pos, coe_eq_zero, coe_lt_coe, ne.def],
id                  └─────────┘                └─────┘  └─────────┘  └────────┘  └────┘
src      └─────────┘└─────────┘└┘            └┘└─────┘└┘└─────────┘└┘└────────┘└┘└────┘
typ      └─────────┘└─────────┘└┘└──────────┘└┘└─────┘└┘└─────────┘└┘└────────┘└┘└────┘
doc      └─────────┘           └┘            └┘       └┘           └┘          └┘      
txt      └─────────┘           └┘            └┘       └┘           └┘          └┘      
par      └─────────┘           └┘            └┘       └┘           └┘          └┘      
pid          └──┘└┘           └┘            └┘       └┘           └┘          └┘      
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
487      assume h₁ h₂, apply nnreal.sub_lt_self, exact zero_lt_iff_ne_zero.2 h₂
id                           └────────────────┘        └─────────────────┘   └┘
src      └──────────┘  └────┘└────────────────┘  └────┘└─────────────────┘└─┘  
typ      └──────────┘  └────┘└────────────────┘  └────┘└─────────────────┘└─┘└┘
doc      └──────────┘  └────┘                    └────┘                   └─┘  
txt      └──────────┘  └────┘                    └────┘                   └─┘  
par      └──────────┘  └────┘                    └────┘                   └─┘  
pid      └──────────┘                                                   └─┘  
st   ───────────────┘└────────────────────────┘└────────────────────────────────
488    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
489  end
490  
491  @[simp] lemma sub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
id                                               
src                                                
typ                                              
doc    └──┘
492  by simpa [-ennreal.sub_le_iff_le_add] using @ennreal.sub_le_iff_le_add a b 0
id                                                └───────────────────────┘  
src     └───────────────────────────────────────┘ └───────────────────────┘  └──
typ     └───────────────────────────────────────┘ └───────────────────────┘└──
doc     └───────────────────────────────────────┘                            └──
txt     └───────────────────────────────────────┘                            └──
par     └───────────────────────────────────────┘                            └──
pid          └──────────────────────────┘└────┘                            └─
st     └──────────────────────────────────────────────────────────────────────────
493  
src  
typ  
doc  
txt  
par  
pid  
st   
494  @[simp] lemma zero_lt_sub_iff_lt : 0 < a - b ↔ b < a :=
id                                               
src                                                
typ                                              
doc    └──┘
495  by simpa [ennreal.bot_lt_iff_ne_bot, -sub_eq_zero_iff_le] using not_iff_not.2 (@sub_eq_zero_iff_le a b)
id             └───────────────────────┘                             └─────────┘     └────────────────┘  
src     └─────┘└───────────────────────┘└───────────────────────────┘└─────────┘└─┘  └────────────────┘  └─
typ     └─────┘└───────────────────────┘└───────────────────────────┘└─────────┘└─┘  └────────────────┘└─
doc     └─────┘                         └───────────────────────────┘           └─┘                      └─
txt     └─────┘                         └───────────────────────────┘           └─┘                      └─
par     └─────┘                         └───────────────────────────┘           └─┘                      └─
pid                                   └────────────────────┘└────┘           └─┘                      
st     └─────────────────────────────────────────────────────────────────────────────────────────────────────
496  
src  
typ  
doc  
txt  
par  
pid  
st   
497  lemma sub_le_self (a b : ennreal) : a - b ≤ a :=
id                            └─────┘        
src                           └─────┘         
typ                           └─────┘        
doc                           └─────┘
498  ennreal.sub_le_iff_le_add.2 $ le_add_of_nonneg_right' $ zero_le _
id   └───────────────────────┘    └─────────────────────┘   └─────┘
src  └───────────────────────┘    └─────────────────────┘   └─────┘
typ  └───────────────────────┘    └─────────────────────┘   └─────┘
499  
500  @[simp] lemma sub_zero : a - 0 = a :=
id                                 
src                                
typ                                
doc    └──┘
501  eq.trans (add_zero (a - 0)).symm $ by simp
id   └──────┘  └──────┘       └──┘
src  └──────┘  └──────┘        └──┘       └────
typ  └──────┘  └──────┘       └──┘       └────
doc                                        └────
txt                                        └────
par                                        └────
pid                                            
st                                        └─────
502  
src  
typ  
doc  
txt  
par  
pid  
st   
503  /-- A version of triangle inequality for difference as a "distance". -/
504  lemma sub_le_sub_add_sub : a - c ≤ a - b + (b - c) :=
id                                         
src                                            
typ                                        
505  ennreal.sub_le_iff_le_add.2 $
id   └───────────────────────┘
src  └───────────────────────┘
typ  └───────────────────────┘
506  calc a ≤ a - b + b : le_sub_add_self
id                  └─────────────┘
src                     └─────────────┘
typ                 └─────────────┘
507  ... ≤ a - b + ((b - c) + c) : add_le_add_left' le_sub_add_self
id                        └──────────────┘ └─────────────┘
src                            └──────────────┘ └─────────────┘
typ                       └──────────────┘ └─────────────┘
508  ... = a - b + (b - c) + c : (add_assoc _ _ _).symm
id                       └───────┘       └──┘
src                           └───────┘       └──┘
typ                      └───────┘       └──┘
509  
510  lemma sub_sub_cancel (h : a < ∞) (h2 : b ≤ a) : a - (a - b) = b :=
id                                                     
src                                                         
typ                                                    
doc                                
511  by rw [← add_right_inj (lt_of_le_of_lt (sub_le_self _ _) h),
id            └───────────┘  └────────────┘  └─────────┘      
src     └────┘└───────────┘ └────────────┘ └─────────┘└────┘ └──
typ     └────┘└───────────┘ └────────────┘ └─────────┘└────┘└──
doc     └────┘                                        └────┘ └──
txt     └────┘                                        └────┘ └──
par     └────┘                                        └────┘ └──
pid       └──┘                                        └────┘ └──
st     └───────────────────────────────────────────────────────┘└─
512    sub_add_cancel_of_le (sub_le_self _ _), add_sub_cancel_of_le h2]
id     └──────────────────┘  └─────────┘       └──────────────────┘ └┘
src  ─┘└──────────────────┘ └─────────┘└─────┘└──────────────────┘  └─
typ  ─┘└──────────────────┘ └─────────┘└─────┘└──────────────────┘└┘└─
doc  ─┘                                └─────┘                      └─
txt  ─┘                                └─────┘                      └─
par  ─┘                                └─────┘                      └─
pid  ─┘                                └─────┘                      
st   ───────────────────────────────────────┘└───────────────────────┘
513  
src  
typ  
doc  
txt  
par  
pid  
st   
514  lemma sub_left_inj {a b c : ennreal} (ha : a < ⊤) (hb : b ≤ a) (hc : c ≤ a) :
id                               └─────┘                              
src                              └─────┘                                 
typ                              └─────┘                              
doc                              └─────┘
515    a - b = a - c ↔ b = c :=
id               
src                  
typ              
516  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
517    begin
st     └─────
518      assume h, have : a - (a - b) = a - (a - c), rw h,
id                                                 
src      └──────┘  └─────┘     └┘        └─┘
typ      └──────┘  └─────┘    └┘      └─┘
doc      └──────┘  └─────┘      └┘         └─┘
txt      └──────┘  └─────┘      └┘         └─┘
par      └──────┘  └─────┘      └┘         └─┘
pid      └──────┘  └───┘└┘      └┘           
st   ───────────┘└────────────────────────────────┘└────┘└─
519      rw [sub_sub_cancel ha hb, sub_sub_cancel ha hc] at this, exact this
id           └────────────┘ └┘ └┘  └────────────┘ └┘ └┘                 └──┘
src      └──┘└────────────┘    └┘└────────────┘    └───────┘  └────┘    
typ      └──┘└────────────┘└┘└┘└┘└────────────┘└┘└┘└───────┘  └────┘└──┘
doc      └──┘                  └┘                  └───────┘  └────┘    
txt      └──┘                  └┘                  └───────┘  └────┘    
par      └──┘                  └┘                  └───────┘  └────┘    
pid        └┘                  └┘                  └──────┘           
st   ───────────────────────────┘└────────────────────┘└──────┘└────────────
520    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
521    (λ h, by rw h)
id                
src             └─┘
typ            └─┘
doc             └─┘
txt             └─┘
par             └─┘
pid               
st             └───┘
522  
523  lemma sub_mul (hc : c ≠ ∞) : (a - b) * c = a * c - b * c :=
id                                           
src                                                
typ                                          
doc                          
524  begin
st   └─────
525    cases le_or_lt a b with hab hab,
id           └──────┘  
src    └────┘└──────┘  └───────────┘
typ    └────┘└──────┘└───────────┘
doc    └────┘          └───────────┘
txt    └────┘          └───────────┘
par    └────┘          └───────────┘
pid                   └───────────┘
st   ────────────────────────────────┘└─
526    { simp [hab, mul_right_mono hab] },
id             └─┘  └────────────┘ └─┘
src      └────┘   └┘└────────────┘   └┘
typ      └────┘└─┘└┘└────────────┘└─┘└┘
doc      └────┘   └┘                 └┘
txt      └────┘   └┘                 └┘
par      └────┘   └┘                 └┘
pid             └┘                 
st   ───┘└─────────────────────────────┘└┘
527    symmetry,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
st   ─────────┘└─
528    apply sub_eq_of_add_eq,
id           └──────────────┘
src    └────┘└──────────────┘
typ    └────┘└──────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ───────────────────────┘└─
529    { exact mul_ne_top (ne_top_of_lt hab) hc },
id             └────────┘  └──────────┘ └─┘  └┘
src      └────┘└────────┘ └──────────┘   └┘  
typ      └────┘└────────┘ └──────────┘└─┘└┘└┘
doc      └────┘                          └┘  
txt      └────┘                          └┘  
par      └────┘                          └┘  
pid                                     └┘  
st   ───┘└─────────────────────────────────────┘└┘
530    rw [← add_mul, sub_add_cancel_of_le (le_of_lt hab)]
id           └─────┘  └──────────────────┘  └──────┘ └─┘
src    └────┘└─────┘└┘└──────────────────┘ └──────┘   └─┘
typ    └────┘└─────┘└┘└──────────────────┘ └──────┘└─┘└─┘
doc    └────┘       └┘                                └─┘
txt    └────┘       └┘                                └─┘
par    └────┘       └┘                                └─┘
pid      └──┘       └┘                                └┘
st   ──────────────┘└───────────────────────────────────┘
531  end
st   └─┘
532  
533  lemma mul_sub (ha : a ≠ ∞) : a * (b - c) = a * b - a * c :=
id                                           
src                                                
typ                                          
doc                          
534  by { simp only [mul_comm a], exact sub_mul ha }
id                   └──────┘          └─────┘ └┘
src       └─────────┘└──────┘   └────┘└─────┘  
typ       └─────────┘└──────┘  └────┘└─────┘└┘
doc       └─────────┘           └────┘         
txt       └─────────┘           └────┘         
par       └─────────┘           └────┘         
pid           └──┘└┘                         
st     └───────────────────────┘└─────────────────┘└┘
535  
536  end sub
537  
538  section sum
539  
540  open finset
541  
542  /-- sum of finte numbers is still finite -/
543  lemma sum_lt_top [decidable_eq α] {s : finset α} {f : α → ennreal} :
id                     └──────────┘        └────┘           └─────┘
src                    └──────────┘         └────┘             └─────┘
typ                    └──────────┘        └────┘           └─────┘
doc                                         └────┘             └─────┘
544    (∀a∈s, f a < ⊤) → s.sum f < ⊤ :=
id                 └──┘   
src                    └──┘    
typ                └──┘   
545  with_top.sum_lt_top
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
doc  └─────────────────┘
546  
547  /-- sum of finte numbers is still finite -/
548  lemma sum_lt_top_iff [decidable_eq α] {s : finset α} {f : α → ennreal} :
id                         └──────────┘        └────┘           └─────┘
src                        └──────────┘         └────┘             └─────┘
typ                        └──────────┘        └────┘           └─────┘
doc                                             └────┘             └─────┘
549    s.sum f < ⊤ ↔ (∀a∈s, f a < ⊤) :=
id     └──┘             
src     └──┘                  
typ    └──┘             
550  with_top.sum_lt_top_iff
id   └─────────────────────┘
src  └─────────────────────┘
typ  └─────────────────────┘
doc  └─────────────────────┘
551  
552  /-- seeing `ennreal` as `nnreal` does not change their sum, unless one of the `ennreal` is infinity -/
553  lemma to_nnreal_sum [decidable_eq α] {s : finset α} {f : α → ennreal} (hf : ∀a∈s, f a < ⊤) :
id                        └──────────┘        └────┘           └─────┘               
src                       └──────────┘         └────┘             └─────┘                   
typ                       └──────────┘        └────┘           └─────┘               
doc                                            └────┘             └─────┘
554    ennreal.to_nnreal (s.sum f) = s.sum (λa, ennreal.to_nnreal (f a)) :=
id     └───────────────┘  └──┘    └──┘     └───────────────┘   
src    └───────────────┘   └──┘      └──┘      └───────────────┘
typ    └───────────────┘  └──┘    └──┘     └───────────────┘   
doc    └───────────────┘                        └───────────────┘
555  begin
st   └─────
556    rw [← coe_eq_coe, coe_to_nnreal, coe_finset_sum, sum_congr],
id           └────────┘  └───────────┘  └────────────┘  └───────┘
src    └────┘└────────┘└┘└───────────┘└┘└────────────┘└┘└───────┘
typ    └────┘└────────┘└┘└───────────┘└┘└────────────┘└┘└───────┘
doc    └────┘          └┘             └┘              └┘         
txt    └────┘          └┘             └┘              └┘         
par    └────┘          └┘             └┘              └┘         
pid      └──┘          └┘             └┘              └┘         
st   ─────────────────┘└─────────────┘└──────────────┘└─────────┘└─
557    { refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ───┘└───┘└┘
558    { intros x hx, rw coe_to_nnreal, rw ← ennreal.lt_top_iff_ne_top, exact hf x hx },
id                       └───────────┘       └───────────────────────┘        └┘  └┘
src      └─────────┘  └─┘└───────────┘  └───┘└───────────────────────┘  └────┘     
typ      └─────────┘  └─┘└───────────┘  └───┘└───────────────────────┘  └────┘└┘└┘
doc      └─────────┘  └─┘               └───┘                           └────┘     
txt      └─────────┘  └─┘               └───┘                           └────┘     
par      └─────────┘  └─┘               └───┘                           └────┘     
pid            └───┘                     └─┘                                     
st   ───┘└─────────┘└────────────────┘└──────────────────────────────┘└──────────────┘└┘
559    { rw ← ennreal.lt_top_iff_ne_top, exact sum_lt_top hf }
id            └───────────────────────┘        └────────┘ └┘
src      └───┘└───────────────────────┘  └────┘└────────┘  
typ      └───┘└───────────────────────┘  └────┘└────────┘└┘
doc      └───┘                           └────┘└────────┘  
txt      └───┘                           └────┘            
par      └───┘                           └────┘            
pid        └─┘                                            
st   ─────────────────────────────────┘└────────────────────┘└─
560  end
st   ──┘
561  
562  /-- seeing `ennreal` as `real` does not change their sum, unless one of the `ennreal` is infinity -/
563  lemma to_real_sum [decidable_eq α] {s : finset α} {f : α → ennreal} (hf : ∀a∈s, f a < ⊤) :
id                      └──────────┘        └────┘           └─────┘               
src                     └──────────┘         └────┘             └─────┘                   
typ                     └──────────┘        └────┘           └─────┘               
doc                                          └────┘             └─────┘
564    ennreal.to_real (s.sum f) = s.sum (λa, ennreal.to_real (f a)) :=
id     └─────────────┘  └──┘    └──┘     └─────────────┘   
src    └─────────────┘   └──┘      └──┘      └─────────────┘
typ    └─────────────┘  └──┘    └──┘     └─────────────┘   
doc    └─────────────┘                        └─────────────┘
565  by { rw [ennreal.to_real, to_nnreal_sum hf, nnreal.coe_sum], refl }
id            └─────────────┘  └───────────┘ └┘  └────────────┘
src       └──┘└─────────────┘└┘└───────────┘  └┘└────────────┘  └───┘
typ       └──┘└─────────────┘└┘└───────────┘└┘└┘└────────────┘  └───┘
doc       └──┘└─────────────┘└┘└───────────┘  └┘                └───┘
txt       └──┘               └┘               └┘                └───┘
par       └──┘               └┘               └┘                └───┘
pid         └┘               └┘               └┘                    
st     └────────────────────┘└────────────────┘└──────────────┘└──────┘└┘
566  
567  end sum
568  
569  section interval
570  
571  variables {x y z : ennreal} {ε ε₁ ε₂ : ennreal} {s : set ennreal}
id                      └─────┘             └─────┘       └─┘ └─────┘
src                     └─────┘             └─────┘       └─┘ └─────┘
typ                     └─────┘             └─────┘       └─┘ └─────┘
doc                     └─────┘             └─────┘           └─────┘
572  
573  protected lemma Ico_eq_Iio : (Ico 0 y) = (Iio y) :=
id                                 └─┘       └─┘ 
src                                └─┘        └─┘
typ                                └─┘       └─┘ 
doc                                └─┘         └─┘
574  ext $ assume a, iff.intro
id   └─┘            └───────┘
src  └─┘             └───────┘
typ  └─┘            └───────┘
575    (assume ⟨_, hx⟩, hx)
id                └┘
typ               └┘
576    (assume hx, ⟨zero_le _, hx⟩)
id             └┘   └─────┘    └┘
src                 └─────┘
typ            └┘   └─────┘    └┘
577  
578  lemma mem_Iio_self_add : x ≠ ⊤ → 0 < ε → x ∈ Iio (x + ε) :=
id                                         └─┘    
src                                           └─┘    
typ                                        └─┘    
doc                                               └─┘
579  assume xt ε0, lt_add_right (by rwa lt_top_iff_ne_top) ε0
id          └┘ └┘  └──────────┘         └───────────────┘  └┘
src                └──────────┘     └──┘└───────────────┘
typ         └┘ └┘  └──────────┘     └──┘└───────────────┘  └┘
doc                                 └──┘
txt                                 └──┘
par                                 └──┘
pid                                    
st                                 └────────────────────┘
580  
581  lemma not_mem_Ioo_self_sub : x = 0 → x ∉ Ioo (x - ε) y :=
id                                        └─┘      
src                                         └─┘    
typ                                       └─┘      
doc                                           └─┘
582  assume x0, by simp [x0]
id          └┘           └┘
src                └────┘  └─
typ         └┘     └────┘└┘└─
doc                └────┘  └─
txt                └────┘  └─
par                └────┘  └─
pid                      
st                └──────────
583  
src  
typ  
doc  
txt  
par  
pid  
st   
584  lemma mem_Ioo_self_sub_add : x ≠ ⊤ → x ≠ 0 → 0 < ε₁ → 0 < ε₂ → x ∈ Ioo (x - ε₁) (x + ε₂) :=
id                                              └┘      └┘     └─┘    └┘     └┘
src                                                               └─┘            
typ                                             └┘      └┘     └─┘    └┘     └┘
doc                                                                     └─┘
585  assume xt x0 ε0 ε0',
id          └┘ └┘ └┘ └─┘
typ         └┘ └┘ └┘ └─┘
586    ⟨ennreal.sub_lt_sub_self xt x0 ε0, lt_add_right (by rwa [lt_top_iff_ne_top]) ε0'⟩
id      └─────────────────────┘ └┘ └┘ └┘  └──────────┘          └───────────────┘   └─┘
src     └─────────────────────┘           └──────────┘     └───┘└───────────────┘
typ     └─────────────────────┘ └┘ └┘ └┘  └──────────┘     └───┘└───────────────┘  └─┘
doc                                                        └───┘                 
txt                                                        └───┘                 
par                                                        └───┘                 
pid                                                           └┘                 
st                                                        └─────────────────────┘
587  
588  end interval
589  
590  section bit
591  
592  @[simp] lemma bit0_inj : bit0 a = bit0 b ↔ a = b :=
id                            └──┘   └──┘     
src                           └──┘    └──┘      
typ                           └──┘   └──┘     
doc    └──┘
593  ⟨λh, begin
id     
typ    
st        └─────
594    rcases (lt_trichotomy a b) with h₁| h₂| h₃,
id             └───────────┘  
src    └─────┘ └───────────┘  └───────────────┘
typ    └─────┘ └───────────┘└───────────────┘
doc    └─────┘                └───────────────┘
txt    └─────┘                └───────────────┘
par    └─────┘                └───────────────┘
pid                          └───────────────┘
st   ───────────────────────────────────────────┘└─
595    { exact (absurd h (ne_of_lt (add_lt_add h₁ h₁))) },
id              └────┘   └──────┘  └────────┘    └┘
src      └────┘ └────┘  └──────┘ └────────┘    └──┘
typ      └────┘ └────┘ └──────┘ └────────┘  └┘└──┘
doc      └────┘                                └──┘
txt      └────┘                                └──┘
par      └────┘                                └──┘
pid                                           └─┘
st   ───┘└─────────────────────────────────────────────┘└┘
596    { exact h₂ },
id             └┘
src      └────┘  
typ      └────┘└┘
doc      └────┘  
txt      └────┘  
par      └────┘  
pid             
st   ───┘└───────┘└┘
597    { exact (absurd h.symm (ne_of_lt (add_lt_add h₃ h₃))) }
id              └────┘ └────┘  └──────┘  └────────┘    └┘
src      └────┘ └────┘└────┘ └──────┘ └────────┘    └──┘
typ      └────┘ └────┘└────┘ └──────┘ └────────┘  └┘└──┘
doc      └────┘                                     └──┘
txt      └────┘                                     └──┘
par      └────┘                                     └──┘
pid                                                └─┘
st   ───────────────────────────────────────────────────────┘└─
598  end,
st   ──┘
599  λh, congr_arg _ h⟩
id      └───────┘   
src      └───────┘
typ     └───────┘   
600  
601  @[simp] lemma bit0_eq_zero_iff : bit0 a = 0 ↔ a = 0 :=
id                                    └──┘       
src                                   └──┘         
typ                                   └──┘       
doc    └──┘
602  by simpa only [bit0_zero] using @bit0_inj a 0
id                  └───────┘         └──────┘ 
src     └──────────┘└───────┘└──────┘ └──────┘ └──
typ     └──────────┘└───────┘└──────┘ └──────┘└──
doc     └──────────┘         └──────┘          └──
txt     └──────────┘         └──────┘          └──
par     └──────────┘         └──────┘          └──
pid          └──┘└┘         └────┘          └─
st     └───────────────────────────────────────────
603  
src  
typ  
doc  
txt  
par  
pid  
st   
604  @[simp] lemma bit0_eq_top_iff : bit0 a = ∞ ↔ a = ∞ :=
id                                   └──┘       
src                                  └──┘         
typ                                  └──┘       
doc    └──┘                                          
605  by rw [bit0, add_eq_top, or_self]
id          └──┘  └────────┘  └─────┘
src     └──┘└──┘└┘└────────┘└┘└─────┘└─
typ     └──┘└──┘└┘└────────┘└┘└─────┘└─
doc     └──┘    └┘          └┘       └─
txt     └──┘    └┘          └┘       └─
par     └──┘    └┘          └┘       └─
pid       └┘    └┘          └┘       
st     └───────┘└──────────┘└───────┘
606  
src  
typ  
doc  
txt  
par  
pid  
st   
607  @[simp] lemma bit1_inj : bit1 a = bit1 b ↔ a = b :=
id                            └──┘   └──┘     
src                           └──┘    └──┘      
typ                           └──┘   └──┘     
doc    └──┘
608  ⟨λh, begin
id     
typ    
st        └─────
609    unfold bit1 at h,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └───┘└───┘
st   ─────────────────┘└─
610    rwa [add_right_inj, bit0_inj] at h,
id          └───────────┘  └──────┘
src    └───┘└───────────┘└┘└──────┘└────┘
typ    └───┘└───────────┘└┘└──────┘└────┘
doc    └───┘             └┘        └────┘
txt    └───┘             └┘        └────┘
par    └───┘             └┘        └────┘
pid       └┘             └┘        └───┘
st   ───────────────────┘└────────┘└───┘└─
611    simp [lt_top_iff_ne_top]
id           └───────────────┘
src    └────┘└───────────────┘└┘
typ    └────┘└───────────────┘└┘
doc    └────┘                 └┘
txt    └────┘                 └┘
par    └────┘                 └┘
pid                         
st   ──────────────────────────┘
612  end,
st   └─┘
613  λh, congr_arg _ h⟩
id      └───────┘   
src      └───────┘
typ     └───────┘   
614  
615  @[simp] lemma bit1_ne_zero : bit1 a ≠ 0 :=
id                                └──┘  
src                               └──┘   
typ                               └──┘  
doc    └──┘
616  by unfold bit1; simp
src     └─────────┘  └────
typ     └─────────┘  └────
doc     └─────────┘  └────
txt     └─────────┘  └────
par     └─────────┘  └────
pid           └───┘      
st     └──────────────────
617  
src  
typ  
doc  
txt  
par  
pid  
st   
618  @[simp] lemma bit1_eq_one_iff : bit1 a = 1 ↔ a = 0 :=
id                                   └──┘       
src                                  └──┘         
typ                                  └──┘       
doc    └──┘
619  by simpa only [bit1_zero] using @bit1_inj a 0
id                  └───────┘         └──────┘ 
src     └──────────┘└───────┘└──────┘ └──────┘ └──
typ     └──────────┘└───────┘└──────┘ └──────┘└──
doc     └──────────┘         └──────┘          └──
txt     └──────────┘         └──────┘          └──
par     └──────────┘         └──────┘          └──
pid          └──┘└┘         └────┘          └─
st     └───────────────────────────────────────────
620  
src  
typ  
doc  
txt  
par  
pid  
st   
621  @[simp] lemma bit1_eq_top_iff : bit1 a = ∞ ↔ a = ∞ :=
id                                   └──┘       
src                                  └──┘         
typ                                  └──┘       
doc    └──┘                                          
622  by unfold bit1; rw add_eq_top; simp
id                      └────────┘
src     └─────────┘  └─┘└────────┘  └────
typ     └─────────┘  └─┘└────────┘  └────
doc     └─────────┘  └─┘            └────
txt     └─────────┘  └─┘            └────
par     └─────────┘  └─┘            └────
pid           └───┘                    
st     └───────────────┘└────────┘└──────
623  
src  
typ  
doc  
txt  
par  
pid  
st   
624  end bit
625  
626  section inv
627  instance : has_inv ennreal := ⟨λa, Inf {b | 1 ≤ a * b}⟩
id              └─────┘ └─────┘        └─┘         
src             └─────┘ └─────┘         └─┘          
typ             └─────┘ └─────┘        └─┘         
doc                     └─────┘         └─┘
628  instance : has_div ennreal := ⟨λa b, a * b⁻¹⟩
id              └─────┘ └─────┘           └┘
src             └─────┘ └─────┘               └┘
typ             └─────┘ └─────┘           └┘
doc                     └─────┘
629  
630  lemma div_def : a / b = a * b⁻¹ := rfl
id                         └┘    └─┘
src                            └┘    └─┘
typ                        └┘    └─┘
631  
632  @[simp] lemma inv_zero : (0 : ennreal)⁻¹ = ∞ :=
id                                 └─────┘ └┘  
src                                └─────┘ └┘  
typ                                └─────┘ └┘  
doc    └──┘                        └─────┘      
633  show Inf {b : ennreal | 1 ≤ 0 * b} = ∞, by simp; refl
id        └─┘     └─────┘            
src       └─┘     └─────┘                  └──┘  └────
typ       └─┘     └─────┘                 └──┘  └────
doc       └─┘      └─────┘                     └──┘  └────
txt                                             └──┘  └────
par                                             └──┘  └────
pid                                                       
st                                             └───────────
634  
src  
typ  
doc  
txt  
par  
pid  
st   
635  @[simp] lemma inv_top : (∞ : ennreal)⁻¹ = 0 :=
id                               └─────┘ └┘ 
src                              └─────┘ └┘ 
typ                              └─────┘ └┘ 
doc    └──┘                      └─────┘
636  bot_unique $ le_of_forall_le_of_dense $ λ a (h : a > 0), Inf_le $ by simp [*, ne_of_gt h, top_mul]
id   └────────┘   └──────────────────────┘                 └────┘               └──────┘   └─────┘
src  └────────┘   └──────────────────────┘                   └────┘      └───────┘└──────┘ └┘└─────┘└─
typ  └────────┘   └──────────────────────┘                 └────┘      └───────┘└──────┘└┘└─────┘└─
doc                                                                       └───────┘         └┘       └─
txt                                                                       └───────┘         └┘       └─
par                                                                       └───────┘         └┘       └─
pid                                                                           └──┘         └┘       
st                                                                       └──────────────────────────────
637  
src  
typ  
doc  
txt  
par  
pid  
st   
638  @[simp] lemma coe_inv (hr : r ≠ 0) : (↑r⁻¹ : ennreal) = (↑r)⁻¹ :=
id                                       └┘   └─────┘     └┘
src                                        └┘   └─────┘      └┘
typ                                      └┘   └─────┘     └┘
doc    └──┘                                       └─────┘
639  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
640    (le_Inf $ assume b (hb : 1 ≤ ↑r * b), coe_le_iff.2 $
id      └────┘                         └────────┘
src     └────┘                            └────────┘
typ     └────┘                         └────────┘
641      by rintros b rfl; rwa [← coe_mul, ← coe_one, coe_le_coe, ← nnreal.inv_le hr] at hb)
id                                └─────┘    └─────┘  └────────┘    └───────────┘ └┘
src         └───────────┘  └─────┘└─────┘└──┘└─────┘└┘└────────┘└──┘└───────────┘  └─────┘
typ         └───────────┘  └─────┘└─────┘└──┘└─────┘└┘└────────┘└──┘└───────────┘└┘└─────┘
doc         └───────────┘  └─────┘       └──┘       └┘          └──┘               └─────┘
txt         └───────────┘  └─────┘       └──┘       └┘          └──┘               └─────┘
par         └───────────┘  └─────┘       └──┘       └┘          └──┘               └─────┘
pid                └────┘     └──┘       └──┘       └┘          └──┘               └────┘
st         └───────────────────┘└───────┘└─────────┘└──────────┘└──────────────────┘└────┘
642    (Inf_le $ by simp; rw [← coe_mul, nnreal.mul_inv_cancel hr]; exact le_refl 1)
id      └────┘                  └─────┘  └───────────────────┘ └┘         └─────┘
src     └────┘      └──┘  └────┘└─────┘└┘└───────────────────┘    └────┘└─────┘└┘
typ     └────┘      └──┘  └────┘└─────┘└┘└───────────────────┘└┘  └────┘└─────┘└┘
doc                 └──┘  └────┘       └┘                         └────┘       └┘
txt                 └──┘  └────┘       └┘                         └────┘       └┘
par                 └──┘  └────┘       └┘                         └────┘       └┘
pid                         └──┘       └┘                                     
st                 └─────────┘└───────┘└────────────────────────┘└───────────────┘
643  
644  @[elim_cast] lemma coe_inv_two : ((2⁻¹:nnreal):ennreal) = 2⁻¹ :=
id                                       └┘ └────┘  └─────┘    └┘
src                                      └┘ └────┘  └─────┘    └┘
typ                                      └┘ └────┘  └─────┘    └┘
doc    └───────┘                            └────┘  └─────┘
645  by rw [coe_inv (ne_of_gt zero_lt_two), coe_two]
id          └─────┘  └──────┘ └─────────┘   └─────┘
src     └──┘└─────┘ └──────┘└─────────┘└─┘└─────┘└─
typ     └──┘└─────┘ └──────┘└─────────┘└─┘└─────┘└─
doc     └──┘                └─────────┘└─┘       └─
txt     └──┘                           └─┘       └─
par     └──┘                           └─┘       └─
pid       └┘                           └─┘       
st     └─────────────────────────────────┘└───────┘
646  
src  
typ  
doc  
txt  
par  
pid  
st   
647  @[simp, elim_cast] lemma coe_div (hr : r ≠ 0) : (↑(p / r) : ennreal) = p / r :=
id                                                         └─────┘     
src                                                           └─────┘     
typ                                                        └─────┘     
doc    └──┘  └───────┘                                           └─────┘
648  show ↑(p * r⁻¹) = ↑p * (↑r)⁻¹, by rw [coe_mul, coe_inv hr]
id           └┘       └┘         └─────┘  └─────┘ └┘
src            └┘         └┘     └──┘└─────┘└┘└─────┘  └─
typ          └┘       └┘     └──┘└─────┘└┘└─────┘└┘└─
doc                                    └──┘       └┘         └─
txt                                    └──┘       └┘         └─
par                                    └──┘       └┘         └─
pid                                      └┘       └┘         
st                                    └──────────┘└──────────┘
649  
src  
typ  
doc  
txt  
par  
pid  
st   
650  @[simp] lemma inv_one : (1:ennreal)⁻¹ = 1 :=
id                              └─────┘ └┘ 
src                             └─────┘ └┘ 
typ                             └─────┘ └┘ 
doc    └──┘                     └─────┘
651  by simpa only [coe_inv one_ne_zero, coe_one] using coe_eq_coe.2 nnreal.inv_one
id                  └─────┘ └─────────┘  └─────┘        └────────┘   └────────────┘
src     └──────────┘└─────┘└─────────┘└┘└─────┘└──────┘└────────┘└─┘└────────────┘
typ     └──────────┘└─────┘└─────────┘└┘└─────┘└──────┘└────────┘└─┘└────────────┘
doc     └──────────┘                  └┘       └──────┘          └─┘              
txt     └──────────┘                  └┘       └──────┘          └─┘              
par     └──────────┘                  └┘       └──────┘          └─┘              
pid          └──┘└┘                  └┘       └────┘          └─┘              
st     └────────────────────────────────────────────────────────────────────────────
652  
src  
typ  
doc  
txt  
par  
pid  
st   
653  protected lemma inv_pow' {n : ℕ} : (a^n)⁻¹ = (a⁻¹)^n :=
id                                       └┘   └┘ 
src                                        └┘    └┘ 
typ                                      └┘   └┘ 
654  begin
st   └─────
655    by_cases a = 0; cases a; cases n; simp [*, none_eq_top, some_eq_coe,
id                                            └─────────┘  └─────────┘
src    └───────┘ └┘  └────┘   └────┘   └───────┘└─────────┘└┘└─────────┘└─
typ    └───────┘└┘  └────┘  └────┘  └───────┘└─────────┘└┘└─────────┘└─
doc    └───────┘  └┘  └────┘   └────┘   └───────┘           └┘           └─
txt    └───────┘  └┘  └────┘   └────┘   └───────┘           └┘           └─
par    └───────┘  └┘  └────┘   └────┘   └───────┘           └┘           └─
pid                                    └──┘           └┘           └─
st   ───────────────────────────────────────────────────────────────────────
656      zero_pow, top_pow, nat.zero_lt_succ] at *,
id       └──────┘  └─────┘  └──────────────┘
src  ───┘└──────┘└┘└─────┘└┘└──────────────┘└────┘
typ  ───┘└──────┘└┘└─────┘└┘└──────────────┘└────┘
doc  ───┘        └┘       └┘                └────┘
txt  ───┘        └┘       └┘                └────┘
par  ───┘        └┘       └┘                └────┘
pid  ───┘        └┘       └┘                └──┘
st   ────────────────────────────────────────────┘└─
657    rw [← coe_inv h, ← coe_pow, ← coe_inv, nnreal.inv_pow', coe_pow],
id           └─────┘     └─────┘    └─────┘  └─────────────┘  └─────┘
src    └────┘└─────┘ └──┘└─────┘└──┘└─────┘└┘└─────────────┘└┘└─────┘
typ    └────┘└─────┘└──┘└─────┘└──┘└─────┘└┘└─────────────┘└┘└─────┘
doc    └────┘        └──┘       └──┘       └┘               └┘       
txt    └────┘        └──┘       └──┘       └┘               └┘       
par    └────┘        └──┘       └──┘       └┘               └┘       
pid      └──┘        └──┘       └──┘       └┘               └┘       
st   ────────────────┘└─────────┘└─────────┘└───────────────┘└───────┘└─
658    rw [← ne.def] at h,
id           └────┘
src    └────┘└────┘└────┘
typ    └────┘└────┘└────┘
doc    └────┘      └────┘
txt    └────┘      └────┘
par    └────┘      └────┘
pid      └──┘      └───┘
st   ─────────────┘└───┘└─
659    rw [← zero_lt_iff_ne_zero] at *,
id           └─────────────────┘
src    └────┘└─────────────────┘└────┘
typ    └────┘└─────────────────┘└────┘
doc    └────┘                   └────┘
txt    └────┘                   └────┘
par    └────┘                   └────┘
pid      └──┘                   └───┘
st   ──────────────────────────┘└───┘└─
660    apply pow_pos h
id           └─────┘ 
src    └────┘└─────┘ 
typ    └────┘└─────┘
doc    └────┘        
txt    └────┘        
par    └────┘        
pid                 
st   ─────────────────┘
661  end
st   └─┘
662  
663  @[simp] lemma inv_inv : (a⁻¹)⁻¹ = a :=
id                            └┘ └┘  
src                            └┘ └┘ 
typ                           └┘ └┘  
doc    └──┘
664  by by_cases a = 0; cases a; simp [*, none_eq_top, some_eq_coe,
id                                     └─────────┘  └─────────┘
src     └───────┘ └┘  └────┘   └───────┘└─────────┘└┘└─────────┘└─
typ     └───────┘└┘  └────┘  └───────┘└─────────┘└┘└─────────┘└─
doc     └───────┘  └┘  └────┘   └───────┘           └┘           └─
txt     └───────┘  └┘  └────┘   └───────┘           └┘           └─
par     └───────┘  └┘  └────┘   └───────┘           └┘           └─
pid                             └──┘           └┘           └─
st     └────────────────────────────────────────────────────────────
665    -coe_inv, (coe_inv _).symm] at *
id                └─────┘
src  ───────────┘ └─────┘└──────────────
typ  ───────────┘ └─────┘└──────────────
doc  ───────────┘        └──────────────
txt  ───────────┘        └──────────────
par  ───────────┘        └──────────────
pid  ───────────┘        └───────┘└──┘
st   ───────────────────────────────────
666  
src  
typ  
doc  
txt  
par  
pid  
st   
667  lemma inv_involutive : function.involutive (λ a:ennreal, a⁻¹) :=
id                          └─────────────────┘      └─────┘  └┘
src                         └─────────────────┘      └─────┘   └┘
typ                         └─────────────────┘      └─────┘  └┘
doc                         └─────────────────┘      └─────┘
668  λ a, ennreal.inv_inv
id       └─────────────┘
src       └─────────────┘
typ      └─────────────┘
669  
670  lemma inv_bijective : function.bijective (λ a:ennreal, a⁻¹) :=
id                         └────────────────┘      └─────┘  └┘
src                        └────────────────┘      └─────┘   └┘
typ                        └────────────────┘      └─────┘  └┘
doc                                                └─────┘
671  ennreal.inv_involutive.bijective
id   └────────────────────┘└────────┘
src  └────────────────────┘└────────┘
typ  └────────────────────┘└────────┘
672  
673  @[simp] lemma inv_eq_inv : a⁻¹ = b⁻¹ ↔ a = b := inv_bijective.1.eq_iff
id                              └┘  └┘        └───────────┘ └────┘
src                              └┘   └┘          └───────────┘ └────┘
typ                             └┘  └┘        └───────────┘ └────┘
doc    └──┘
674  
675  @[simp] lemma inv_eq_top : a⁻¹ = ∞ ↔ a = 0 :=
id                              └┘     
src                              └┘      
typ                             └┘     
doc    └──┘                           
676  inv_zero ▸ inv_eq_inv
id   └──────┘  └────────┘
src  └──────┘  └────────┘
typ  └──────┘  └────────┘
677  
678  lemma inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
id                      └┘     
src                      └┘               └────
typ                     └┘              └────
doc                                          └────
txt                                           └────
par                                           └────
pid                                               
st                                           └─────
679  
src  
typ  
doc  
txt  
par  
pid  
st   
680  @[simp] lemma inv_eq_zero : a⁻¹ = 0 ↔ a = ∞ :=
id                               └┘       
src                               └┘        
typ                              └┘       
doc    └──┘                                    
681  inv_top ▸ inv_eq_inv
id   └─────┘  └────────┘
src  └─────┘  └────────┘
typ  └─────┘  └────────┘
682  
683  lemma inv_ne_zero : a⁻¹ ≠ 0 ↔ a ≠ ∞ := by simp
id                       └┘       
src                       └┘               └────
typ                      └┘              └────
doc                                           └────
txt                                            └────
par                                            └────
pid                                                
st                                            └─────
684  
src  
typ  
doc  
txt  
par  
pid  
st   
685  @[simp] lemma inv_pos : 0 < a⁻¹ ↔ a ≠ ∞ :=
id                              └┘    
src                              └┘     
typ                             └┘    
doc    └──┘                                
686  zero_lt_iff_ne_zero.trans inv_ne_zero
id   └─────────────────┘└────┘ └─────────┘
src  └─────────────────┘└────┘ └─────────┘
typ  └─────────────────┘└────┘ └─────────┘
687  
688  @[simp] lemma inv_lt_inv : a⁻¹ < b⁻¹ ↔ b < a :=
id                              └┘  └┘    
src                              └┘   └┘    
typ                             └┘  └┘    
doc    └──┘
689  begin
st   └─────
690    cases a; cases b; simp only [some_eq_coe, none_eq_top, inv_top],
id                                └─────────┘  └─────────┘  └─────┘
src    └────┘   └────┘   └─────────┘└─────────┘└┘└─────────┘└┘└─────┘
typ    └────┘  └────┘  └─────────┘└─────────┘└┘└─────────┘└┘└─────┘
doc    └────┘   └────┘   └─────────┘           └┘           └┘       
txt    └────┘   └────┘   └─────────┘           └┘           └┘       
par    └────┘   └────┘   └─────────┘           └┘           └┘       
pid                        └──┘└┘           └┘           └┘       
st   ────────────────────────────────────────────────────────────────┘└─
691    { simp only [lt_irrefl] },
id                  └───────┘
src      └─────────┘└───────┘└┘
typ      └─────────┘└───────┘└┘
doc      └─────────┘         └┘
txt      └─────────┘         └┘
par      └─────────┘         └┘
pid          └──┘└┘         
st   ───┘└────────────────────┘└┘
692    { exact inv_pos.trans lt_top_iff_ne_top.symm },
id             └───────────┘ └────────────────────┘
src      └────┘└───────────┘└────────────────────┘
typ      └────┘└───────────┘└────────────────────┘
doc      └────┘                                   
txt      └────┘                                   
par      └────┘                                   
pid                                              
st   ───┘└─────────────────────────────────────────┘└┘
693    { simp only [not_lt_zero, not_top_lt] },
id                  └─────────┘  └────────┘
src      └─────────┘└─────────┘└┘└────────┘└┘
typ      └─────────┘└─────────┘└┘└────────┘└┘
doc      └─────────┘           └┘          └┘
txt      └─────────┘           └┘          └┘
par      └─────────┘           └┘          └┘
pid          └──┘└┘           └┘          
st   ───┘└──────────────────────────────────┘└┘
694    { cases eq_or_lt_of_le (zero_le a) with ha ha;
id             └────────────┘  └─────┘ 
src      └────┘└────────────┘ └─────┘ └──────────┘
typ      └────┘└────────────┘ └─────┘└──────────┘
doc      └────┘                       └──────────┘
txt      └────┘                       └──────────┘
par      └────┘                       └──────────┘
pid                                  └─────────┘
st   ─────────────────────────────────────────────────
695        cases eq_or_lt_of_le (zero_le b) with hb hb,
id               └────────────┘  └─────┘ 
src        └────┘└────────────┘ └─────┘ └──────────┘
typ        └────┘└────────────┘ └─────┘└──────────┘
doc        └────┘                       └──────────┘
txt        └────┘                       └──────────┘
par        └────┘                       └──────────┘
pid                                    └─────────┘
st   ────────────────────────────────────────────────┘└─
696      { subst a, subst b, simp },
id                       
src        └────┘   └────┘   └───┘
typ        └────┘  └────┘  └───┘
doc        └────┘   └────┘   └───┘
txt        └────┘   └────┘   └───┘
par        └────┘   └────┘   └───┘
pid                            
st   ─────┘└─────┘└───────┘└─────┘└┘
697      { subst a, simp },
id               
src        └────┘   └───┘
typ        └────┘  └───┘
doc        └────┘   └───┘
txt        └────┘   └───┘
par        └────┘   └───┘
pid                    
st   ─────┘└─────┘└─────┘└┘
698      { subst b, simp [zero_lt_iff_ne_zero, lt_top_iff_ne_top, inv_ne_top] },
id                       └─────────────────┘  └───────────────┘  └────────┘
src        └────┘   └────┘└─────────────────┘└┘└───────────────┘└┘└────────┘└┘
typ        └────┘  └────┘└─────────────────┘└┘└───────────────┘└┘└────────┘└┘
doc        └────┘   └────┘                   └┘                 └┘          └┘
txt        └────┘   └────┘                   └┘                 └┘          └┘
par        └────┘   └────┘                   └┘                 └┘          └┘
pid                                       └┘                 └┘          
st   ─────┘└─────┘└──────────────────────────────────────────────────────────┘└┘
699      { rw [← coe_inv (ne_of_gt ha), ← coe_inv (ne_of_gt hb), coe_lt_coe, coe_lt_coe],
id               └─────┘  └──────┘ └┘     └─────┘  └──────┘ └┘   └────────┘  └────────┘
src        └────┘└─────┘ └──────┘  └───┘└─────┘ └──────┘  └─┘└────────┘└┘└────────┘
typ        └────┘└─────┘ └──────┘└┘└───┘└─────┘ └──────┘└┘└─┘└────────┘└┘└────────┘
doc        └────┘                  └───┘                  └─┘          └┘          
txt        └────┘                  └───┘                  └─┘          └┘          
par        └────┘                  └───┘                  └─┘          └┘          
pid          └──┘                  └───┘                  └─┘          └┘          
st   ────────────────────────────────┘└───────────────────────┘└──────────┘└──────────┘└─
700        simp only [nnreal.coe_lt.symm] at *,
src        └─────────┘                  └────┘
typ        └─────────┘└────────────────┘└────┘
doc        └─────────┘                  └────┘
txt        └─────────┘                  └────┘
par        └─────────┘                  └────┘
pid            └──┘└┘                  └──┘
st   ────────────────────────────────────────┘└─
701        exact inv_lt_inv ha hb } }
id               └────────┘ └┘ └┘
src        └────┘└────────┘    
typ        └────┘└────────┘└┘└┘
doc        └────┘              
txt        └────┘              
par        └────┘              
pid                           
st   ────────────────────────────┘└───
702  end
st   ──┘
703  
704  lemma inv_lt_iff_inv_lt : a⁻¹ < b ↔ b⁻¹ < a :=
id                             └┘    └┘  
src                             └┘      └┘ 
typ                            └┘    └┘  
705  by simpa only [inv_inv] using @inv_lt_inv a b⁻¹
id                  └─────┘         └────────┘  └┘
src     └──────────┘└─────┘└──────┘ └────────┘  └┘
typ     └──────────┘└─────┘└──────┘ └────────┘└┘
doc     └──────────┘       └──────┘               
txt     └──────────┘       └──────┘               
par     └──────────┘       └──────┘               
pid          └──┘└┘       └────┘               
st     └─────────────────────────────────────────────
706  
src  
typ  
doc  
txt  
par  
pid  
st   
707  lemma lt_inv_iff_lt_inv : a < b⁻¹ ↔ b < a⁻¹ :=
id                               └┘    └┘
src                                └┘      └┘
typ                              └┘    └┘
708  by simpa only [inv_inv] using @inv_lt_inv a⁻¹ b
id                  └─────┘         └────────┘ └┘ 
src     └──────────┘└─────┘└──────┘ └────────┘ └┘ 
typ     └──────────┘└─────┘└──────┘ └────────┘└┘
doc     └──────────┘       └──────┘               
txt     └──────────┘       └──────┘               
par     └──────────┘       └──────┘               
pid          └──┘└┘       └────┘               
st     └─────────────────────────────────────────────
709  
src  
typ  
doc  
txt  
par  
pid  
st   
710  @[simp] lemma inv_le_inv : a⁻¹ ≤ b⁻¹ ↔ b ≤ a :=
id                              └┘  └┘    
src                              └┘   └┘    
typ                             └┘  └┘    
doc    └──┘
711  by simp only [le_iff_lt_or_eq, inv_lt_inv, inv_eq_inv, eq_comm]
id                 └─────────────┘  └────────┘  └────────┘  └─────┘
src     └─────────┘└─────────────┘└┘└────────┘└┘└────────┘└┘└─────┘└─
typ     └─────────┘└─────────────┘└┘└────────┘└┘└────────┘└┘└─────┘└─
doc     └─────────┘               └┘          └┘          └┘       └─
txt     └─────────┘               └┘          └┘          └┘       └─
par     └─────────┘               └┘          └┘          └┘       └─
pid         └──┘└┘               └┘          └┘          └┘       
st     └─────────────────────────────────────────────────────────────
712  
src  
typ  
doc  
txt  
par  
pid  
st   
713  lemma inv_le_iff_inv_le : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
id                             └┘    └┘  
src                             └┘      └┘ 
typ                            └┘    └┘  
714  by simpa only [inv_inv] using @inv_le_inv a b⁻¹
id                  └─────┘         └────────┘  └┘
src     └──────────┘└─────┘└──────┘ └────────┘  └┘
typ     └──────────┘└─────┘└──────┘ └────────┘└┘
doc     └──────────┘       └──────┘               
txt     └──────────┘       └──────┘               
par     └──────────┘       └──────┘               
pid          └──┘└┘       └────┘               
st     └─────────────────────────────────────────────
715  
src  
typ  
doc  
txt  
par  
pid  
st   
716  lemma le_inv_iff_le_inv : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
id                               └┘    └┘
src                                └┘      └┘
typ                              └┘    └┘
717  by simpa only [inv_inv] using @inv_le_inv a⁻¹ b
id                  └─────┘         └────────┘ └┘ 
src     └──────────┘└─────┘└──────┘ └────────┘ └┘ 
typ     └──────────┘└─────┘└──────┘ └────────┘└┘
doc     └──────────┘       └──────┘               
txt     └──────────┘       └──────┘               
par     └──────────┘       └──────┘               
pid          └──┘└┘       └────┘               
st     └─────────────────────────────────────────────
718  
src  
typ  
doc  
txt  
par  
pid  
st   
719  @[simp] lemma inv_lt_one : a⁻¹ < 1 ↔ 1 < a :=
id                              └┘        
src                              └┘       
typ                             └┘        
doc    └──┘
720  inv_lt_iff_inv_lt.trans $ by rw [inv_one]
id   └───────────────┘└────┘          └─────┘
src  └───────────────┘└────┘      └──┘└─────┘└─
typ  └───────────────┘└────┘      └──┘└─────┘└─
doc                               └──┘       └─
txt                               └──┘       └─
par                               └──┘       └─
pid                                 └┘       
st                               └──────────┘
721  
src  
typ  
doc  
txt  
par  
pid  
st   
722  lemma top_div : ∞ / a = if a = ∞ then 0 else ∞ :=
id                                         
src                                          
typ                                        
doc                                             
723  by by_cases a = ∞; simp [div_def, top_mul, *]
id                         └─────┘  └─────┘
src     └───────┘   └────┘└─────┘└┘└─────┘└────
typ     └───────┘  └────┘└─────┘└┘└─────┘└────
doc     └───────┘     └────┘       └┘       └────
txt     └───────┘     └────┘       └┘       └────
par     └───────┘     └────┘       └┘       └────
pid                             └┘       └──┘
st     └───────────────────────────────────────────
724  
src  
typ  
doc  
txt  
par  
pid  
st   
725  @[simp] lemma div_top : a / ∞ = 0 := by simp only [div_def, inv_top, mul_zero]
id                                                  └─────┘  └─────┘  └──────┘
src                                       └─────────┘└─────┘└┘└─────┘└┘└──────┘└─
typ                                      └─────────┘└─────┘└┘└─────┘└┘└──────┘└─
doc    └──┘                                 └─────────┘       └┘       └┘        └─
txt                                          └─────────┘       └┘       └┘        └─
par                                          └─────────┘       └┘       └┘        └─
pid                                              └──┘└┘       └┘       └┘        
st                                          └───────────────────────────────────────
726  
src  
typ  
doc  
txt  
par  
pid  
st   
727  @[simp] lemma zero_div : 0 / a = 0 := zero_mul a⁻¹
id                                      └──────┘ └┘
src                                      └──────┘  └┘
typ                                     └──────┘ └┘
doc    └──┘
728  
729  lemma le_div_iff_mul_le : ∀{b}, b ≠ 0 → b ≠ ⊤ → (a ≤ c / b ↔ a * b ≤ c)
id                                                       
src                                                              
typ                                                      
730  | none     h0 ht := (ht rfl).elim
id     └──┘        └┘        └─┘ └──┘
src    └──┘                  └─┘ └──┘
typ    └──┘        └┘        └─┘ └──┘
731  | (some r) h0 ht :=
id      └──┘
src     └──┘
typ     └──┘
732    begin
st     └─────
733      have hr : r ≠ 0, from mt coe_eq_coe.2 h0,
id                           └┘ └────────┘   └┘
src      └────────┘ └┘  └───┘└┘└────────┘└─┘
typ      └────────┘└┘  └───┘└┘└────────┘└─┘└┘
doc      └────────┘  └┘  └───┘            └─┘
txt      └────────┘  └┘  └───┘            └─┘
par      └────────┘  └┘  └───┘            └─┘
pid      └─────┘└─┘    └───┘            └─┘
st   ──────────────────┘└───────────────────────┘└─
734      rw [← ennreal.mul_le_mul_left h0 ht],
id             └─────────────────────┘ └┘ └┘
src      └────┘└─────────────────────┘    
typ      └────┘└─────────────────────┘└┘└┘
doc      └────┘                           
txt      └────┘                           
par      └────┘                           
pid        └──┘                           
st   ──────────────────────────────────────┘└──
735      suffices : ↑r * a ≤ (↑r  * ↑r⁻¹) * c ↔ a * ↑r ≤ c,
id                                 └┘               
src      └─────────┘     └┘   └┘└┘        
typ      └─────────┘     └┘   └┘└┘      
doc      └─────────┘        └┘     └┘        
txt      └─────────┘        └┘     └┘        
par      └─────────┘        └┘     └┘        
pid      └───────┘└┘        └┘     └┘        
st   ────────────────────────────────────────────────────┘└─
736      { simpa [some_eq_coe, div_def, hr, mul_left_comm, mul_comm, mul_assoc] },
id                └─────────┘  └─────┘  └┘  └───────────┘  └──────┘  └───────┘
src        └─────┘└─────────┘└┘└─────┘└┘  └┘└───────────┘└┘└──────┘└┘└───────┘└┘
typ        └─────┘└─────────┘└┘└─────┘└┘└┘└┘└───────────┘└┘└──────┘└┘└───────┘└┘
doc        └─────┘           └┘       └┘  └┘             └┘        └┘         └┘
txt        └─────┘           └┘       └┘  └┘             └┘        └┘         └┘
par        └─────┘           └┘       └┘  └┘             └┘        └┘         └┘
pid                        └┘       └┘  └┘             └┘        └┘         
st   ─────┘└───────────────────────────────────────────────────────────────────┘└┘
737      rw [← coe_mul, nnreal.mul_inv_cancel hr, coe_one, one_mul, mul_comm]
id             └─────┘  └───────────────────┘ └┘  └─────┘  └─────┘  └──────┘
src      └────┘└─────┘└┘└───────────────────┘  └┘└─────┘└┘└─────┘└┘└──────┘└─
typ      └────┘└─────┘└┘└───────────────────┘└┘└┘└─────┘└┘└─────┘└┘└──────┘└─
doc      └────┘       └┘                       └┘       └┘       └┘        └─
txt      └────┘       └┘                       └┘       └┘       └┘        └─
par      └────┘       └┘                       └┘       └┘       └┘        └─
pid        └──┘       └┘                       └┘       └┘       └┘        
st   ────────────────┘└────────────────────────┘└───────┘└───────┘└────────┘
738    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
739  
740  lemma div_le_iff_le_mul (hb0 : b ≠ 0) (hbt : b ≠ ⊤) : a / b ≤ c ↔ a ≤ c * b :=
id                                                              
src                                                                   
typ                                                             
741  suffices a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹, by simpa [div_def],
id              └┘        └┘            └─────┘
src               └┘            └┘     └─────┘└─────┘
typ             └┘        └┘     └─────┘└─────┘
doc                                         └─────┘       
txt                                         └─────┘       
par                                         └─────┘       
pid                                                     
st                                         └──────────────┘
742  (le_div_iff_mul_le (inv_ne_zero.2 hbt) (inv_ne_top.2 hb0)).symm
id    └───────────────┘  └─────────┘  └─┘   └────────┘  └─┘  └──┘
src   └───────────────┘  └─────────┘        └────────┘       └──┘
typ   └───────────────┘  └─────────┘  └─┘   └────────┘  └─┘  └──┘
743  
744  lemma inv_le_iff_le_mul : (b = ⊤ → a ≠ 0) → (a = ⊤ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b) :=
id                                                      └┘         
src                                                            └┘          
typ                                                     └┘         
745  begin
st   └─────
746    cases a; cases b; simp [none_eq_top, some_eq_coe, mul_top, top_mul] {contextual := tt},
id                           └─────────┘  └─────────┘  └─────┘  └─────┘                 └┘
src    └────┘   └────┘   └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└┘ └────────────┘└┘
typ    └────┘  └────┘  └────┘└─────────┘└┘└─────────┘└┘└─────┘└┘└─────┘└┘ └────────────┘└┘
doc    └────┘   └────┘   └────┘           └┘           └┘       └┘       └┘ └────────────┘  
txt    └────┘   └────┘   └────┘           └┘           └┘       └┘       └┘ └────────────┘  
par    └────┘   └────┘   └────┘           └┘           └┘       └┘       └┘ └────────────┘  
pid                                   └┘           └┘       └┘        └────────────┘  
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
747    by_cases a = 0; simp [*, -coe_mul, coe_mul.symm, -coe_inv, (coe_inv _).symm, nnreal.inv_le]
id                                                               └─────┘          └───────────┘
src    └───────┘ └┘  └─────────────────┘            └──────────┘ └─────┘└────────┘└───────────┘└┘
typ    └───────┘└┘  └─────────────────┘└──────────┘└──────────┘ └─────┘└────────┘└───────────┘└┘
doc    └───────┘  └┘  └─────────────────┘            └──────────┘        └────────┘             └┘
txt    └───────┘  └┘  └─────────────────┘            └──────────┘        └────────┘             └┘
par    └───────┘  └┘  └─────────────────┘            └──────────┘        └────────┘             └┘
pid                    └────────────┘            └──────────┘        └────────┘             
st   ─────────────────────────────────────────────────────────────────────────────────────────────┘
748  end
st   └─┘
749  
750  @[simp] lemma le_inv_iff_mul_le : a ≤ b⁻¹ ↔ a * b ≤ 1 :=
id                                       └┘     
src                                        └┘       
typ                                      └┘     
doc    └──┘
751  begin
st   └─────
752    cases b, { by_cases a = 0; simp [*, none_eq_top, mul_top] },
id                                      └─────────┘  └─────┘
src    └────┘     └───────┘ └┘  └───────┘└─────────┘└┘└─────┘└┘
typ    └────┘    └───────┘└┘  └───────┘└─────────┘└┘└─────┘└┘
doc    └────┘     └───────┘  └┘  └───────┘           └┘       └┘
txt    └────┘     └───────┘  └┘  └───────┘           └┘       └┘
par    └────┘     └───────┘  └┘  └───────┘           └┘       └┘
pid                              └──┘           └┘       
st   ────────┘└──┘└─────────────────────────────────────────────┘└┘
753    by_cases b = 0; simp [*, some_eq_coe, le_div_iff_mul_le],
id                             └─────────┘  └───────────────┘
src    └───────┘  └┘  └───────┘└─────────┘└┘└───────────────┘
typ    └───────┘ └┘  └───────┘└─────────┘└┘└───────────────┘
doc    └───────┘  └┘  └───────┘           └┘                 
txt    └───────┘  └┘  └───────┘           └┘                 
par    └───────┘  └┘  └───────┘           └┘                 
pid                    └──┘           └┘                 
st   ─────────────────────────────────────────────────────────┘└─
754    suffices : a ≤ 1 / b ↔ a * b ≤ 1, { simpa [div_def, h] },
id                                           └─────┘  
src    └─────────┘ └─┘     └┘    └─────┘└─────┘└┘ └┘
typ    └─────────┘ └─┘   └┘    └─────┘└─────┘└┘└┘
doc    └─────────┘  └─┘       └┘    └─────┘       └┘ └┘
txt    └─────────┘  └─┘       └┘    └─────┘       └┘ └┘
par    └─────────┘  └─┘       └┘    └─────┘       └┘ └┘
pid    └───────┘└┘  └─┘                       └┘ 
st   ─────────────────────────────────┘└──┘└─────────────────┘└┘
755    exact le_div_iff_mul_le (mt coe_eq_coe.1 h) coe_ne_top
id           └───────────────┘  └┘ └────────┘     └────────┘
src    └────┘└───────────────┘ └┘└────────┘└─┘ └┘└────────┘
typ    └────┘└───────────────┘ └┘└────────┘└─┘└┘└────────┘
doc    └────┘                              └─┘ └┘          
txt    └────┘                              └─┘ └┘          
par    └────┘                              └─┘ └┘          
pid                                       └─┘ └┘          
st   ────────────────────────────────────────────────────────┘
756  end
st   └─┘
757  
758  lemma mul_inv_cancel (h0 : a ≠ 0) (ht : a ≠ ⊤) : a * a⁻¹ = 1 :=
id                                                 └┘ 
src                                                    └┘ 
typ                                                └┘ 
759  begin
st   └─────
760    lift a to nnreal using ht,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
761    norm_cast at h0,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid             └────┘
st   ────────────────┘└─
762    rw [← coe_inv h0],
id           └─────┘ └┘
src    └────┘└─────┘  
typ    └────┘└─────┘└┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid      └──┘         
st   ─────────────────┘└──
763    norm_cast,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
764    exact nnreal.mul_inv_cancel h0
id           └───────────────────┘ └┘
src    └────┘└───────────────────┘  
typ    └────┘└───────────────────┘└┘
doc    └────┘                       
txt    └────┘                       
par    └────┘                       
pid                                
st   ────────────────────────────────┘
765  end
st   └─┘
766  
767  lemma inv_mul_cancel (h0 : a ≠ 0) (ht : a ≠ ∞) : a⁻¹ * a = 1 :=
id                                               └┘   
src                                                 └┘    
typ                                              └┘   
doc                                              
768  mul_comm a a⁻¹ ▸ mul_inv_cancel h0 ht
id   └──────┘  └┘  └────────────┘ └┘ └┘
src  └──────┘    └┘  └────────────┘
typ  └──────┘  └┘  └────────────┘ └┘ └┘
769  
770  lemma mul_le_iff_le_inv {a b r : ennreal} (hr₀ : r ≠ 0) (hr₁ : r ≠ ⊤) : (r * a ≤ b ↔ a ≤ r⁻¹ * b) :=
id                                    └─────┘                                    └┘  
src                                   └─────┘                                           └┘ 
typ                                   └─────┘                                    └┘  
doc                                   └─────┘
771  by rw [← @ennreal.mul_le_mul_left _ a _ hr₀ hr₁, ← mul_assoc, mul_inv_cancel hr₀ hr₁, one_mul]
id             └─────────────────────┘      └─┘ └─┘    └───────┘  └────────────┘ └─┘ └─┘  └─────┘
src     └────┘ └─────────────────────┘└─┘ └─┘      └──┘└───────┘└┘└────────────┘      └┘└─────┘└─
typ     └────┘ └─────────────────────┘└─┘└─┘└─┘└─┘└──┘└───────┘└┘└────────────┘└─┘└─┘└┘└─────┘└─
doc     └────┘                        └─┘ └─┘      └──┘         └┘                    └┘       └─
txt     └────┘                        └─┘ └─┘      └──┘         └┘                    └┘       └─
par     └────┘                        └─┘ └─┘      └──┘         └┘                    └┘       └─
pid       └──┘                        └─┘ └─┘      └──┘         └┘                    └┘       
st     └───────────────────────────────────────────┘└───────────┘└──────────────────────┘└───────┘
772  
src  
typ  
doc  
txt  
par  
pid  
st   
773  lemma le_of_forall_lt_one_mul_lt : ∀{x y : ennreal}, (∀a<1, a * x ≤ y) → x ≤ y :=
id                                              └─────┘                   
src                                             └─────┘                      
typ                                             └─────┘                   
doc                                             └─────┘
774  forall_ennreal.2 $ and.intro
id   └────────────┘    └───────┘
src  └────────────┘    └───────┘
typ  └────────────┘    └───────┘
775    (assume r, forall_ennreal.2 $ and.intro
id               └────────────┘    └───────┘
src               └────────────┘    └───────┘
typ              └────────────┘    └───────┘
776      (assume q h, coe_le_coe.2 $ nnreal.le_of_forall_lt_one_mul_lt $ assume a ha,
id                  └────────┘    └───────────────────────────────┘           └┘
src                   └────────┘    └───────────────────────────────┘
typ                 └────────┘    └───────────────────────────────┘           └┘
777        begin rw [← coe_le_coe, coe_mul], exact h _ (coe_lt_coe.2 ha) end)
id                     └────────┘  └─────┘             └────────┘   └┘
src              └────┘└────────┘└┘└─────┘  └────┘ └─┘ └────────┘└─┘  └┘
typ              └────┘└────────┘└┘└─────┘  └────┘└─┘ └────────┘└─┘└┘└┘
doc              └────┘          └┘         └────┘ └─┘           └─┘  └┘
txt              └────┘          └┘         └────┘ └─┘           └─┘  └┘
par              └────┘          └┘         └────┘ └─┘           └─┘  └┘
pid                └──┘          └┘               └─┘           └─┘  
st         └────────────────────┘└───────┘└─────────────────────────────┘└─┘
778      (assume h, le_top))
id                 └────┘
src                 └────┘
typ                └────┘
779    (assume r hr,
id              └┘
typ             └┘
780      have ((1 / 2 : nnreal) : ennreal) * ⊤ ≤ r :=
id                     └────┘    └─────┘     
src                    └────┘    └─────┘    
typ                    └────┘    └─────┘     
doc                     └────┘    └─────┘
781        hr _ (coe_lt_coe.2 ((@nnreal.coe_lt (1/2) 1).1 one_half_lt_one)),
id         └┘    └────────┘     └───────────┘          └─────────────┘
src              └────────┘     └───────────┘          └─────────────┘
typ        └┘    └────────┘     └───────────┘          └─────────────┘
782      have ne : ((1 / 2 : nnreal) : ennreal) ≠ 0,
id                          └────┘    └─────┘  
src                         └────┘    └─────┘  
typ                         └────┘    └─────┘  
doc                          └────┘    └─────┘
783      begin
st       └─────
784        rw [(≠), coe_eq_zero],
id                 └─────────┘
src        └──┘└──┘└─────────┘
typ        └──┘└──┘└─────────┘
doc        └──┘ └──┘           
txt        └──┘ └──┘           
par        └──┘ └──┘           
pid          └┘ └──┘           
st   ────────────┘└───────────┘└──
785        refine zero_lt_iff_ne_zero.1 _,
id                └─────────────────┘
src        └─────┘└─────────────────┘└──┘
typ        └─────┘└─────────────────┘└──┘
doc        └─────┘                   └──┘
txt        └─────┘                   └──┘
par        └─────┘                   └──┘
pid                                 └──┘
st   ───────────────────────────────────┘└─
786        show 0 < (1 / 2 : ℝ),
id                    
src        └─────┘ └┘└───┘ 
typ        └─────┘ └┘└───┘ 
doc        └─────┘  └┘ └───┘ 
txt        └─────┘  └┘ └───┘ 
par        └─────┘  └┘ └───┘ 
pid        └─────┘  └┘ └───┘ 
st   ─────────────────────────┘└─
787        exact div_pos zero_lt_one _root_.two_pos
id               └─────┘ └─────────┘ └────────────┘
src        └────┘└─────┘└─────────┘└────────────┘
typ        └────┘└─────┘└─────────┘└────────────┘
doc        └────┘                                
txt        └────┘                                
par        └────┘                                
pid                                             
st   ───────────────────────────────────────────────
788      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
789      by rwa [mul_top, if_neg ne] at this)
id               └─────┘  └────┘ └┘
src         └───┘└─────┘└┘└────┘└┘└───────┘
typ         └───┘└─────┘└┘└────┘└┘└───────┘
doc         └───┘       └┘        └───────┘
txt         └───┘       └┘        └───────┘
par         └───┘       └┘        └───────┘
pid            └┘       └┘        └──────┘
st         └───────────┘└─────────┘└──────┘
790  
791  lemma div_add_div_same {a b c : ennreal} : a / c + b / c = (a + b) / c :=
id                                   └─────┘                  
src                                  └─────┘                       
typ                                  └─────┘                  
doc                                  └─────┘
792  eq.symm $ right_distrib a b (c⁻¹)
id   └─────┘   └───────────┘    └┘
src  └─────┘   └───────────┘       └┘
typ  └─────┘   └───────────┘    └┘
793  
794  lemma div_self (h0 : a ≠ 0) (hI : a ≠ ∞) : a / a = 1 :=
id                                            
src                                               
typ                                           
doc                                        
795  mul_inv_cancel h0 hI
id   └────────────┘ └┘ └┘
src  └────────────┘
typ  └────────────┘ └┘ └┘
796  
797  lemma mul_div_cancel (h0 : a ≠ 0) (hI : a ≠ ∞) : (b / a) * a = b :=
id                                                       
src                                                          
typ                                                      
doc                                              
798  by rw [div_def, mul_assoc, inv_mul_cancel h0 hI, mul_one]
id          └─────┘  └───────┘  └────────────┘ └┘ └┘  └─────┘
src     └──┘└─────┘└┘└───────┘└┘└────────────┘    └┘└─────┘└─
typ     └──┘└─────┘└┘└───────┘└┘└────────────┘└┘└┘└┘└─────┘└─
doc     └──┘       └┘         └┘                  └┘       └─
txt     └──┘       └┘         └┘                  └┘       └─
par     └──┘       └┘         └┘                  └┘       └─
pid       └┘       └┘         └┘                  └┘       
st     └──────────┘└─────────┘└────────────────────┘└───────┘
799  
src  
typ  
doc  
txt  
par  
pid  
st   
800  lemma mul_div_cancel' (h0 : a ≠ 0) (hI : a ≠ ∞) : a * (b / a) = b :=
id                                                        
src                                                           
typ                                                       
doc                                               
801  by rw [mul_comm, mul_div_cancel h0 hI]
id          └──────┘  └────────────┘ └┘ └┘
src     └──┘└──────┘└┘└────────────┘    └─
typ     └──┘└──────┘└┘└────────────┘└┘└┘└─
doc     └──┘        └┘                  └─
txt     └──┘        └┘                  └─
par     └──┘        └┘                  └─
pid       └┘        └┘                  
st     └───────────┘└────────────────────┘
802  
src  
typ  
doc  
txt  
par  
pid  
st   
803  lemma inv_two_add_inv_two : (2:ennreal)⁻¹ + 2⁻¹ = 1 :=
id                                  └─────┘ └┘   └┘ 
src                                 └─────┘ └┘   └┘ 
typ                                 └─────┘ └┘   └┘ 
doc                                 └─────┘
804  by rw [← two_mul, ← div_def, div_self two_ne_zero two_ne_top]
id            └─────┘    └─────┘  └──────┘ └─────────┘ └────────┘
src     └────┘└─────┘└──┘└─────┘└┘└──────┘└─────────┘└────────┘└─
typ     └────┘└─────┘└──┘└─────┘└┘└──────┘└─────────┘└────────┘└─
doc     └────┘       └──┘       └┘                             └─
txt     └────┘       └──┘       └┘                             └─
par     └────┘       └──┘       └┘                             └─
pid       └──┘       └──┘       └┘                             
st     └────────────┘└─────────┘└───────────────────────────────┘
805  
src  
typ  
doc  
txt  
par  
pid  
st   
806  lemma add_halves (a : ennreal) : a / 2 + a / 2 = a :=
id                         └─────┘              
src                        └─────┘               
typ                        └─────┘              
doc                        └─────┘
807  by rw [div_def, ← mul_add, inv_two_add_inv_two, mul_one]
id          └─────┘    └─────┘  └─────────────────┘  └─────┘
src     └──┘└─────┘└──┘└─────┘└┘└─────────────────┘└┘└─────┘└─
typ     └──┘└─────┘└──┘└─────┘└┘└─────────────────┘└┘└─────┘└─
doc     └──┘       └──┘       └┘                   └┘       └─
txt     └──┘       └──┘       └┘                   └┘       └─
par     └──┘       └──┘       └┘                   └┘       └─
pid       └┘       └──┘       └┘                   └┘       
st     └──────────┘└─────────┘└───────────────────┘└───────┘
808  
src  
typ  
doc  
txt  
par  
pid  
st   
809  @[simp] lemma div_zero_iff {a b : ennreal} : a / b = 0 ↔ a = 0 ∨ b = ⊤ :=
id                                     └─────┘                  
src                                    └─────┘                      
typ                                    └─────┘                  
doc    └──┘                            └─────┘
810  by simp [div_def, mul_eq_zero]
id            └─────┘  └─────────┘
src     └────┘└─────┘└┘└─────────┘└─
typ     └────┘└─────┘└┘└─────────┘└─
doc     └────┘       └┘           └─
txt     └────┘       └┘           └─
par     └────┘       └┘           └─
pid                └┘           
st     └────────────────────────────
811  
src  
typ  
doc  
txt  
par  
pid  
st   
812  @[simp] lemma div_pos_iff {a b : ennreal} : 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤ :=
id                                    └─────┘                  
src                                   └─────┘                      
typ                                   └─────┘                  
doc    └──┘                           └─────┘
813  by simp [zero_lt_iff_ne_zero, not_or_distrib]
id            └─────────────────┘  └────────────┘
src     └────┘└─────────────────┘└┘└────────────┘└─
typ     └────┘└─────────────────┘└┘└────────────┘└─
doc     └────┘                   └┘              └─
txt     └────┘                   └┘              └─
par     └────┘                   └┘              └─
pid                            └┘              
st     └───────────────────────────────────────────
814  
src  
typ  
doc  
txt  
par  
pid  
st   
815  lemma half_pos {a : ennreal} (h : 0 < a) : 0 < a / 2 :=
id                       └─────┘                  
src                      └─────┘                    
typ                      └─────┘                  
doc                      └─────┘
816  by simp [ne_of_gt h]
id            └──────┘ 
src     └────┘└──────┘ └─
typ     └────┘└──────┘└─
doc     └────┘         └─
txt     └────┘         └─
par     └────┘         └─
pid                  
st     └──────────────────
817  
src  
typ  
doc  
txt  
par  
pid  
st   
818  lemma one_half_lt_one : (2⁻¹:ennreal) < 1 := inv_lt_one.2 $ one_lt_two
id                             └┘ └─────┘        └────────┘    └────────┘
src                            └┘ └─────┘        └────────┘    └────────┘
typ                            └┘ └─────┘        └────────┘    └────────┘
doc                               └─────┘
819  
820  lemma half_lt_self {a : ennreal} (hz : a ≠ 0) (ht : a ≠ ⊤) : a / 2 < a :=
id                           └─────┘                              
src                          └─────┘                                
typ                          └─────┘                              
doc                          └─────┘
821  begin
st   └─────
822    lift a to nnreal using ht,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
823    norm_cast at *,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid             └───┘
st   ───────────────┘└─
824    rw [← coe_div _root_.two_ne_zero'], -- `norm_cast` fails to apply `coe_div`
id           └─────┘ └─────────────────┘
src    └────┘└─────┘└─────────────────┘
typ    └────┘└─────┘└─────────────────┘
doc    └────┘                          
txt    └────┘                          
par    └────┘                          
pid      └──┘                          
st   ──────────────────────────────────┘└──────────────────────────────────────────
825    norm_cast,
src    └───────┘
typ    └───────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
st   ──────────┘└─
826    exact nnreal.half_lt_self hz
id           └─────────────────┘ └┘
src    └────┘└─────────────────┘  
typ    └────┘└─────────────────┘└┘
doc    └────┘                     
txt    └────┘                     
par    └────┘                     
pid                              
st   ──────────────────────────────┘
827  end
st   └─┘
828  
829  lemma sub_half (h : a ≠ ∞) : a - a / 2 = a / 2 :=
id                                     
src                                        
typ                                    
doc                          
830  begin
st   └─────
831    lift a to nnreal using h,
id              └────┘       
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ─────────────────────────┘└─
832    exact sub_eq_of_add_eq (mul_ne_top coe_ne_top $ by simp) (add_halves a)
id           └──────────────┘  └────────┘ └────────┘             └────────┘ 
src    └────┘└──────────────┘ └────────┘└────────┘   └──┘└┘ └────────┘ └┘
typ    └────┘└──────────────┘ └────────┘└────────┘   └──┘└┘ └────────┘└┘
doc    └────┘                                        └──┘└┘            └┘
txt    └────┘                                        └──┘└┘            └┘
par    └────┘                                        └──┘└┘            └┘
pid                                                 └─────┘            
st   ───────────────────────────────────────────────────┘└───┘└───────────────┘
833  end
st   └─┘
834  
835  lemma one_sub_inv_two : (1:ennreal) - 2⁻¹ = 2⁻¹ :=
id                              └─────┘    └┘   └┘
src                             └─────┘    └┘   └┘
typ                             └─────┘    └┘   └┘
doc                             └─────┘
836  by simpa only [div_def, one_mul] using sub_half one_ne_top
id                  └─────┘  └─────┘        └──────┘ └────────┘
src     └──────────┘└─────┘└┘└─────┘└──────┘└──────┘└────────┘
typ     └──────────┘└─────┘└┘└─────┘└──────┘└──────┘└────────┘
doc     └──────────┘       └┘       └──────┘                  
txt     └──────────┘       └┘       └──────┘                  
par     └──────────┘       └┘       └──────┘                  
pid          └──┘└┘       └┘       └────┘                  
st     └────────────────────────────────────────────────────────
837  
src  
typ  
doc  
txt  
par  
pid  
st   
838  lemma exists_inv_nat_lt {a : ennreal} (h : a ≠ 0) :
id                                └─────┘        
src                               └─────┘         
typ                               └─────┘        
doc                               └─────┘
839    ∃n:ℕ, (n:ennreal)⁻¹ < a :=
id          └─────┘ └┘  
src          └─────┘ └┘ 
typ         └─────┘ └┘  
doc             └─────┘
840  @inv_inv a ▸ by simp only [inv_lt_inv, ennreal.exists_nat_gt (inv_ne_top.2 h)]
id    └─────┘                 └────────┘  └───────────────────┘  └────────┘   
src   └─────┘       └─────────┘└────────┘└┘└───────────────────┘ └────────┘└─┘ └──
typ   └─────┘      └─────────┘└────────┘└┘└───────────────────┘ └────────┘└─┘└──
doc                  └─────────┘          └┘                                └─┘ └──
txt                  └─────────┘          └┘                                └─┘ └──
par                  └─────────┘          └┘                                └─┘ └──
pid                      └──┘└┘          └┘                                └─┘ └┘
st                  └───────────────────────────────────────────────────────────────
841  
src  
typ  
doc  
txt  
par  
pid  
st   
842  end inv
843  
844  section real
845  
846  lemma to_real_add (ha : a ≠ ⊤) (hb : b ≠ ⊤) : (a+b).to_real = a.to_real + b.to_real :=
id                                             └─────┘   └──────┘  └──────┘
src                                                └─────┘    └──────┘   └──────┘
typ                                            └─────┘   └──────┘  └──────┘
doc                                                     └─────┘     └──────┘    └──────┘
847  begin
st   └─────
848    lift a to nnreal using ha,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
849    lift b to nnreal using hb,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
850    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
851  end
st   └─┘
852  
853  lemma to_real_add_le : (a+b).to_real ≤ a.to_real + b.to_real :=
id                            └─────┘   └──────┘  └──────┘
src                             └─────┘    └──────┘   └──────┘
typ                           └─────┘   └──────┘  └──────┘
doc                              └─────┘     └──────┘    └──────┘
854  if ha : a = ⊤ then by simp only [ha, top_add, top_to_real, zero_add, to_real_nonneg]
id   └┘                            └┘  └─────┘  └─────────┘  └──────┘  └────────────┘
src  └┘                  └─────────┘  └┘└─────┘└┘└─────────┘└┘└──────┘└┘└────────────┘└┘
typ  └┘                 └─────────┘└┘└┘└─────┘└┘└─────────┘└┘└──────┘└┘└────────────┘└┘
doc                        └─────────┘  └┘       └┘           └┘        └┘              └┘
txt                        └─────────┘  └┘       └┘           └┘        └┘              └┘
par                        └─────────┘  └┘       └┘           └┘        └┘              └┘
pid                            └──┘└┘  └┘       └┘           └┘        └┘              
st                        └──────────────────────────────────────────────────────────────┘
855  else if hb : b = ⊤ then by simp only [hb, add_top, top_to_real, add_zero, to_real_nonneg]
id        └┘                            └┘  └─────┘  └─────────┘  └──────┘  └────────────┘
src       └┘                  └─────────┘  └┘└─────┘└┘└─────────┘└┘└──────┘└┘└────────────┘└┘
typ       └┘                 └─────────┘└┘└┘└─────┘└┘└─────────┘└┘└──────┘└┘└────────────┘└┘
doc                             └─────────┘  └┘       └┘           └┘        └┘              └┘
txt                             └─────────┘  └┘       └┘           └┘        └┘              └┘
par                             └─────────┘  └┘       └┘           └┘        └┘              └┘
pid                                 └──┘└┘  └┘       └┘           └┘        └┘              
st                             └──────────────────────────────────────────────────────────────┘
856  else le_of_eq (to_real_add ha hb)
id        └──────┘  └─────────┘ └┘ └┘
src       └──────┘  └─────────┘
typ       └──────┘  └─────────┘ └┘ └┘
857  
858  lemma of_real_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
id                                                  
src                                                 
typ                                                 
859    ennreal.of_real (p + q) = ennreal.of_real p + ennreal.of_real q :=
id     └─────────────┘       └─────────────┘   └─────────────┘ 
src    └─────────────┘         └─────────────┘    └─────────────┘
typ    └─────────────┘       └─────────────┘   └─────────────┘ 
doc    └─────────────┘           └─────────────┘     └─────────────┘
860  by rw [ennreal.of_real, ennreal.of_real, ennreal.of_real, ← coe_add,
id          └─────────────┘  └─────────────┘  └─────────────┘    └─────┘
src     └──┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└──┘└─────┘└─
typ     └──┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└──┘└─────┘└─
doc     └──┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└──┘       └─
txt     └──┘               └┘               └┘               └──┘       └─
par     └──┘               └┘               └┘               └──┘       └─
pid       └┘               └┘               └┘               └──┘       └─
st     └──────────────────┘└───────────────┘└───────────────┘└─────────┘└─
861         coe_eq_coe, nnreal.of_real_add hp hq]
id          └────────┘  └────────────────┘ └┘ └┘
src  ──────┘└────────┘└┘└────────────────┘    └─
typ  ──────┘└────────┘└┘└────────────────┘└┘└┘└─
doc  ──────┘          └┘                      └─
txt  ──────┘          └┘                      └─
par  ──────┘          └┘                      └─
pid  ──────┘          └┘                      
st   ────────────────┘└────────────────────────┘
862  
src  
typ  
doc  
txt  
par  
pid  
st   
863  @[simp] lemma to_real_le_to_real (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a.to_real ≤ b.to_real ↔ a ≤ b :=
id                                                          └──────┘  └──────┘    
src                                                            └──────┘   └──────┘    
typ                                                         └──────┘  └──────┘    
doc    └──┘                                                        └──────┘    └──────┘
864  begin
st   └─────
865    lift a to nnreal using ha,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
866    lift b to nnreal using hb,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
867    norm_cast
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ───────────┘
868  end
st   └─┘
869  
870  @[simp] lemma to_real_lt_to_real (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a.to_real < b.to_real ↔ a < b :=
id                                                          └──────┘  └──────┘    
src                                                            └──────┘   └──────┘    
typ                                                         └──────┘  └──────┘    
doc    └──┘                                                        └──────┘    └──────┘
871  begin
st   └─────
872    lift a to nnreal using ha,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
873    lift b to nnreal using hb,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
874    norm_cast
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid             
st   ───────────┘
875  end
st   └─┘
876  
877  lemma to_real_max (hr : a ≠ ⊤) (hp : b ≠ ⊤) :
id                                       
src                                        
typ                                      
878    ennreal.to_real (max a b) = max (ennreal.to_real a) (ennreal.to_real b) :=
id     └─────────────┘  └─┘     └─┘  └─────────────┘    └─────────────┘ 
src    └─────────────┘  └─┘       └─┘  └─────────────┘     └─────────────┘
typ    └─────────────┘  └─┘     └─┘  └─────────────┘    └─────────────┘ 
doc    └─────────────┘                  └─────────────┘     └─────────────┘
879  (le_total a b).elim
id    └──────┘   └──┘
src   └──────┘     └──┘
typ   └──────┘   └──┘
880    (λ h, by simp only [h, (ennreal.to_real_le_to_real hr hp).2 h, max_eq_right])
id                           └────────────────────────┘ └┘ └┘      └──────────┘
src             └─────────┘ └┘ └────────────────────────┘    └──┘ └┘└──────────┘
typ            └─────────┘└┘ └────────────────────────┘└┘└┘└──┘└┘└──────────┘
doc             └─────────┘ └┘                               └──┘ └┘            
txt             └─────────┘ └┘                               └──┘ └┘            
par             └─────────┘ └┘                               └──┘ └┘            
pid                 └──┘└┘ └┘                               └──┘ └┘            
st             └──────────────────────────────────────────────────────────────────┘
881    (λ h, by simp only [h, (ennreal.to_real_le_to_real hp hr).2 h, max_eq_left])
id                           └────────────────────────┘ └┘ └┘      └─────────┘
src             └─────────┘ └┘ └────────────────────────┘    └──┘ └┘└─────────┘
typ            └─────────┘└┘ └────────────────────────┘└┘└┘└──┘└┘└─────────┘
doc             └─────────┘ └┘                               └──┘ └┘           
txt             └─────────┘ └┘                               └──┘ └┘           
par             └─────────┘ └┘                               └──┘ └┘           
pid                 └──┘└┘ └┘                               └──┘ └┘           
st             └─────────────────────────────────────────────────────────────────┘
882  
883  lemma to_nnreal_pos_iff : 0 < a.to_nnreal ↔ (0 < a ∧ a ≠ ∞) :=
id                                └────────┘          
src                                └────────┘            
typ                               └────────┘          
doc                                 └────────┘                
884  begin
st   └─────
885    cases a,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
886    { simp [none_eq_top] },
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ───┘└─────────────────┘└┘
887    { simp [some_eq_coe] }
id             └─────────┘
src      └────┘└─────────┘└┘
typ      └────┘└─────────┘└┘
doc      └────┘           └┘
txt      └────┘           └┘
par      └────┘           └┘
pid                     
st   ──────────────────────┘└─
888  end
st   ──┘
889  
890  lemma to_real_pos_iff : 0 < a.to_real ↔ (0 < a ∧ a ≠ ∞):=
id                              └──────┘          
src                              └──────┘            
typ                             └──────┘          
doc                               └──────┘                
891  (nnreal.coe_pos).trans to_nnreal_pos_iff
id    └────────────┘ └───┘  └───────────────┘
src   └────────────┘ └───┘  └───────────────┘
typ   └────────────┘ └───┘  └───────────────┘
892  
893  lemma of_real_le_of_real {p q : ℝ} (h : p ≤ q) : ennreal.of_real p ≤ ennreal.of_real q :=
id                                                └─────────────┘   └─────────────┘ 
src                                                 └─────────────┘    └─────────────┘
typ                                               └─────────────┘   └─────────────┘ 
doc                                                   └─────────────┘     └─────────────┘
894  by simp [ennreal.of_real, nnreal.of_real_le_of_real h]
id            └─────────────┘  └───────────────────────┘ 
src     └────┘└─────────────┘└┘└───────────────────────┘ └─
typ     └────┘└─────────────┘└┘└───────────────────────┘└─
doc     └────┘└─────────────┘└┘                          └─
txt     └────┘               └┘                          └─
par     └────┘               └┘                          └─
pid                        └┘                          
st     └────────────────────────────────────────────────────
895  
src  
typ  
doc  
txt  
par  
pid  
st   
896  @[simp] lemma of_real_le_of_real_iff {p q : ℝ} (h : 0 ≤ q) : ennreal.of_real p ≤ ennreal.of_real q ↔ p ≤ q :=
id                                                             └─────────────┘   └─────────────┘     
src                                                             └─────────────┘    └─────────────┘      
typ                                                            └─────────────┘   └─────────────┘     
doc    └──┘                                                       └─────────────┘     └─────────────┘
897  by rw [ennreal.of_real, ennreal.of_real, coe_le_coe, nnreal.of_real_le_of_real_iff h]
id          └─────────────┘  └─────────────┘  └────────┘  └───────────────────────────┘ 
src     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└───────────────────────────┘ └─
typ     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└───────────────────────────┘└─
doc     └──┘└─────────────┘└┘└─────────────┘└┘          └┘                              └─
txt     └──┘               └┘               └┘          └┘                              └─
par     └──┘               └┘               └┘          └┘                              └─
pid       └┘               └┘               └┘          └┘                              
st     └──────────────────┘└───────────────┘└──────────┘└───────────────────────────────┘
898  
src  
typ  
doc  
txt  
par  
pid  
st   
899  @[simp] lemma of_real_lt_of_real_iff {p q : ℝ} (h : 0 < q) : ennreal.of_real p < ennreal.of_real q ↔ p < q :=
id                                                             └─────────────┘   └─────────────┘     
src                                                             └─────────────┘    └─────────────┘      
typ                                                            └─────────────┘   └─────────────┘     
doc    └──┘                                                       └─────────────┘     └─────────────┘
900  by rw [ennreal.of_real, ennreal.of_real, coe_lt_coe, nnreal.of_real_lt_of_real_iff h]
id          └─────────────┘  └─────────────┘  └────────┘  └───────────────────────────┘ 
src     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└───────────────────────────┘ └─
typ     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└───────────────────────────┘└─
doc     └──┘└─────────────┘└┘└─────────────┘└┘          └┘                              └─
txt     └──┘               └┘               └┘          └┘                              └─
par     └──┘               └┘               └┘          └┘                              └─
pid       └┘               └┘               └┘          └┘                              
st     └──────────────────┘└───────────────┘└──────────┘└───────────────────────────────┘
901  
src  
typ  
doc  
txt  
par  
pid  
st   
902  lemma of_real_lt_of_real_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :
id                                                            
src                                                          
typ                                                           
903    ennreal.of_real p < ennreal.of_real q ↔ p < q :=
id     └─────────────┘   └─────────────┘     
src    └─────────────┘    └─────────────┘      
typ    └─────────────┘   └─────────────┘     
doc    └─────────────┘     └─────────────┘
904  by rw [ennreal.of_real, ennreal.of_real, coe_lt_coe, nnreal.of_real_lt_of_real_iff_of_nonneg hp]
id          └─────────────┘  └─────────────┘  └────────┘  └─────────────────────────────────────┘ └┘
src     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└─────────────────────────────────────┘  └─
typ     └──┘└─────────────┘└┘└─────────────┘└┘└────────┘└┘└─────────────────────────────────────┘└┘└─
doc     └──┘└─────────────┘└┘└─────────────┘└┘          └┘                                         └─
txt     └──┘               └┘               └┘          └┘                                         └─
par     └──┘               └┘               └┘          └┘                                         └─
pid       └┘               └┘               └┘          └┘                                         
st     └──────────────────┘└───────────────┘└──────────┘└──────────────────────────────────────────┘
905  
src  
typ  
doc  
txt  
par  
pid  
st   
906  @[simp] lemma of_real_pos {p : ℝ} : 0 < ennreal.of_real p ↔ 0 < p :=
id                                         └─────────────┘      
src                                        └─────────────┘      
typ                                        └─────────────┘      
doc    └──┘                                  └─────────────┘
907  by simp [ennreal.of_real]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘└─────────────┘└─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
908  
src  
typ  
doc  
txt  
par  
pid  
st   
909  @[simp] lemma of_real_eq_zero {p : ℝ} : ennreal.of_real p = 0 ↔ p ≤ 0 :=
id                                          └─────────────┘       
src                                         └─────────────┘         
typ                                         └─────────────┘       
doc    └──┘                                  └─────────────┘
910  by simp [ennreal.of_real]
id            └─────────────┘
src     └────┘└─────────────┘└─
typ     └────┘└─────────────┘└─
doc     └────┘└─────────────┘└─
txt     └────┘               └─
par     └────┘               └─
pid                        
st     └───────────────────────
911  
src  
typ  
doc  
txt  
par  
pid  
st   
912  lemma of_real_le_iff_le_to_real {a : ℝ} {b : ennreal} (hb : b ≠ ⊤) :
id                                               └─────┘          
src                                              └─────┘           
typ                                              └─────┘          
doc                                               └─────┘
913    ennreal.of_real a ≤ b ↔ a ≤ ennreal.to_real b :=
id     └─────────────┘       └─────────────┘ 
src    └─────────────┘          └─────────────┘
typ    └─────────────┘       └─────────────┘ 
doc    └─────────────┘             └─────────────┘
914  begin
st   └─────
915    lift b to nnreal using hb,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
916    simpa [ennreal.of_real, ennreal.to_real] using nnreal.of_real_le_iff_le_coe
id            └─────────────┘  └─────────────┘        └──────────────────────────┘
src    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘
typ    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘
doc    └─────┘└─────────────┘└┘└─────────────┘└──────┘                            
txt    └─────┘               └┘               └──────┘                            
par    └─────┘               └┘               └──────┘                            
pid                        └┘               └────┘                            
st   ─────────────────────────────────────────────────────────────────────────────┘
917  end
st   └─┘
918  
919  lemma of_real_lt_iff_lt_to_real {a : ℝ} {b : ennreal} (ha : 0 ≤ a) (hb : b ≠ ⊤) :
id                                               └─────┘                     
src                                              └─────┘                       
typ                                              └─────┘                     
doc                                               └─────┘
920    ennreal.of_real a < b ↔ a < ennreal.to_real b :=
id     └─────────────┘       └─────────────┘ 
src    └─────────────┘          └─────────────┘
typ    └─────────────┘       └─────────────┘ 
doc    └─────────────┘             └─────────────┘
921  begin
st   └─────
922    lift b to nnreal using hb,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
923    simpa [ennreal.of_real, ennreal.to_real] using nnreal.of_real_lt_iff_lt_coe ha
id            └─────────────┘  └─────────────┘        └──────────────────────────┘ └┘
src    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘  
typ    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘└┘
doc    └─────┘└─────────────┘└┘└─────────────┘└──────┘                              
txt    └─────┘               └┘               └──────┘                              
par    └─────┘               └┘               └──────┘                              
pid                        └┘               └────┘                              
st   ────────────────────────────────────────────────────────────────────────────────┘
924  end
st   └─┘
925  
926  lemma le_of_real_iff_to_real_le {a : ennreal} {b : ℝ} (ha : a ≠ ⊤) (hb : 0 ≤ b) :
id                                        └─────┘                            
src                                       └─────┘                            
typ                                       └─────┘                            
doc                                       └─────┘
927    a ≤ ennreal.of_real b ↔ ennreal.to_real a ≤ b :=
id       └─────────────┘   └─────────────┘   
src       └─────────────┘    └─────────────┘   
typ      └─────────────┘   └─────────────┘   
doc        └─────────────┘     └─────────────┘
928  begin
st   └─────
929    lift a to nnreal using ha,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
930    simpa [ennreal.of_real, ennreal.to_real] using nnreal.le_of_real_iff_coe_le hb
id            └─────────────┘  └─────────────┘        └──────────────────────────┘ └┘
src    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘  
typ    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘└┘
doc    └─────┘└─────────────┘└┘└─────────────┘└──────┘                              
txt    └─────┘               └┘               └──────┘                              
par    └─────┘               └┘               └──────┘                              
pid                        └┘               └────┘                              
st   ────────────────────────────────────────────────────────────────────────────────┘
931  end
st   └─┘
932  
933  lemma to_real_le_of_le_of_real {a : ennreal} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ennreal.of_real b) :
id                                       └─────┘                           └─────────────┘ 
src                                      └─────┘                             └─────────────┘
typ                                      └─────┘                           └─────────────┘ 
doc                                      └─────┘                                └─────────────┘
934    ennreal.to_real a ≤ b :=
id     └─────────────┘   
src    └─────────────┘   
typ    └─────────────┘   
doc    └─────────────┘
935  have ha : a ≠ ⊤, from ne_top_of_le_ne_top of_real_ne_top h,
id                      └─────────────────┘ └────────────┘ 
src                      └─────────────────┘ └────────────┘
typ                     └─────────────────┘ └────────────┘ 
936  (le_of_real_iff_to_real_le ha hb).1 h
id    └───────────────────────┘ └┘ └┘   
src   └───────────────────────┘       
typ   └───────────────────────┘ └┘ └┘   
937  
938  lemma lt_of_real_iff_to_real_lt {a : ennreal} {b : ℝ} (ha : a ≠ ⊤) :
id                                        └─────┘                 
src                                       └─────┘                  
typ                                       └─────┘                 
doc                                       └─────┘
939    a < ennreal.of_real b ↔ ennreal.to_real a < b :=
id       └─────────────┘   └─────────────┘   
src       └─────────────┘    └─────────────┘   
typ      └─────────────┘   └─────────────┘   
doc        └─────────────┘     └─────────────┘
940  begin
st   └─────
941    lift a to nnreal using ha,
id              └────┘       └┘
src    └───┘ └──┘└────┘└─────┘
typ    └───┘└──┘└────┘└─────┘└┘
doc    └───┘ └──┘└────┘└─────┘
txt    └───┘ └──┘      └─────┘
par    └───┘ └──┘      └─────┘
pid         └──┘      └─────┘
st   ──────────────────────────┘└─
942    simpa [ennreal.of_real, ennreal.to_real] using nnreal.lt_of_real_iff_coe_lt
id            └─────────────┘  └─────────────┘        └──────────────────────────┘
src    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘
typ    └─────┘└─────────────┘└┘└─────────────┘└──────┘└──────────────────────────┘
doc    └─────┘└─────────────┘└┘└─────────────┘└──────┘                            
txt    └─────┘               └┘               └──────┘                            
par    └─────┘               └┘               └──────┘                            
pid                        └┘               └────┘                            
st   ─────────────────────────────────────────────────────────────────────────────┘
943  end
st   └─┘
944  
945  lemma of_real_mul {p q : ℝ} (hp : 0 ≤ p) :
id                                       
src                                     
typ                                      
946    ennreal.of_real (p * q) = (ennreal.of_real p) * (ennreal.of_real q) :=
id     └─────────────┘        └─────────────┘     └─────────────┘ 
src    └─────────────┘          └─────────────┘      └─────────────┘
typ    └─────────────┘        └─────────────┘     └─────────────┘ 
doc    └─────────────┘            └─────────────┘       └─────────────┘
947  by { simp only [ennreal.of_real, coe_mul.symm, coe_eq_coe], exact nnreal.of_real_mul hp }
id                   └─────────────┘                └────────┘         └────────────────┘ └┘
src       └─────────┘└─────────────┘└┘            └┘└────────┘  └────┘└────────────────┘  
typ       └─────────┘└─────────────┘└┘└──────────┘└┘└────────┘  └────┘└────────────────┘└┘
doc       └─────────┘└─────────────┘└┘            └┘            └────┘                    
txt       └─────────┘               └┘            └┘            └────┘                    
par       └─────────┘               └┘            └┘            └────┘                    
pid           └──┘└┘               └┘            └┘                                     
st     └──────────────────────────────────────────────────────┘└────────────────────────────┘└┘
948  
949  lemma to_real_of_real_mul (c : ℝ) (a : ennreal) (h : 0 ≤ c) :
id                                         └─────┘          
src                                        └─────┘         
typ                                        └─────┘          
doc                                         └─────┘
950    ennreal.to_real ((ennreal.of_real c) * a) = c * ennreal.to_real a :=
id     └─────────────┘   └─────────────┘         └─────────────┘ 
src    └─────────────┘   └─────────────┘            └─────────────┘
typ    └─────────────┘   └─────────────┘         └─────────────┘ 
doc    └─────────────┘   └─────────────┘               └─────────────┘
951  begin
st   └─────
952    cases a,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
953    { simp only [none_eq_top, ennreal.to_real, top_to_nnreal, nnreal.coe_zero, mul_zero, mul_top],
id                  └─────────┘  └─────────────┘  └───────────┘  └─────────────┘  └──────┘  └─────┘
src      └─────────┘└─────────┘└┘└─────────────┘└┘└───────────┘└┘└─────────────┘└┘└──────┘└┘└─────┘
typ      └─────────┘└─────────┘└┘└─────────────┘└┘└───────────┘└┘└─────────────┘└┘└──────┘└┘└─────┘
doc      └─────────┘           └┘└─────────────┘└┘             └┘               └┘        └┘       
txt      └─────────┘           └┘               └┘             └┘               └┘        └┘       
par      └─────────┘           └┘               └┘             └┘               └┘        └┘       
pid          └──┘└┘           └┘               └┘             └┘               └┘        └┘       
st   ───┘└─────────────────────────────────────────────────────────────────────────────────────────┘└─
954      by_cases h' : c ≤ 0,
id                      
src      └───────┘  └─┘ └┘
typ      └───────┘  └─┘└┘
doc      └───────┘  └─┘  └┘
txt      └───────┘  └─┘  └┘
par      └───────┘  └─┘  └┘
pid                └─┘  
st   ──────────────────────┘└─
955      { rw [if_pos], { simp }, { convert of_real_zero, exact le_antisymm h' h } },
id             └────┘                       └──────────┘        └─────────┘ └┘ 
src        └──┘└────┘    └───┘     └──────┘└──────────┘  └────┘└─────────┘   
typ        └──┘└────┘    └───┘     └──────┘└──────────┘  └────┘└─────────┘└┘
doc        └──┘          └───┘     └──────┘              └────┘              
txt        └──┘          └───┘     └──────┘              └────┘              
par        └──┘          └───┘     └──────┘              └────┘              
pid          └┘                                                           
st   ─────┘└────────┘└───┘└───┘└┘└─────────────────────┘└───────────────────────┘└──┘
956      { rw [if_neg], refl, rw [of_real_eq_zero], assumption } },
id             └────┘             └─────────────┘
src        └──┘└────┘  └──┘  └──┘└─────────────┘  └─────────┘
typ        └──┘└────┘  └──┘  └──┘└─────────────┘  └─────────┘
doc        └──┘        └──┘  └──┘                 └─────────┘
txt        └──┘        └──┘  └──┘                 └─────────┘
par        └──┘        └──┘  └──┘                 └─────────┘
pid          └┘                └┘                           
st   ───────────────┘└─────┘└───────────────────┘└────────────┘└──┘
957    { simp only [ennreal.to_real, ennreal.to_nnreal],
id                  └─────────────┘  └───────────────┘
src      └─────────┘└─────────────┘└┘└───────────────┘
typ      └─────────┘└─────────────┘└┘└───────────────┘
doc      └─────────┘└─────────────┘└┘└───────────────┘
txt      └─────────┘               └┘                 
par      └─────────┘               └┘                 
pid          └──┘└┘               └┘                 
st   ─────────────────────────────────────────────────┘└─
958      simp only [some_eq_coe, ennreal.of_real, coe_mul.symm, to_nnreal_coe, nnreal.coe_mul],
id                  └─────────┘  └─────────────┘                └───────────┘  └────────────┘
src      └─────────┘└─────────┘└┘└─────────────┘└┘            └┘└───────────┘└┘└────────────┘
typ      └─────────┘└─────────┘└┘└─────────────┘└┘└──────────┘└┘└───────────┘└┘└────────────┘
doc      └─────────┘           └┘└─────────────┘└┘            └┘             └┘              
txt      └─────────┘           └┘               └┘            └┘             └┘              
par      └─────────┘           └┘               └┘            └┘             └┘              
pid          └──┘└┘           └┘               └┘            └┘             └┘              
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
959      congr, apply nnreal.coe_of_real, exact h }
id                    └────────────────┘        
src      └───┘  └────┘└────────────────┘  └────┘ 
typ      └───┘  └────┘└────────────────┘  └────┘
doc             └────┘                    └────┘ 
txt      └───┘  └────┘                    └────┘ 
par      └───┘  └────┘                    └────┘ 
pid                                            
st   ────────┘└────────────────────────┘└────────┘└─
960  end
st   ──┘
961  
962  @[simp] lemma to_real_mul_top (a : ennreal) : ennreal.to_real (a * ⊤) = 0 :=
id                                      └─────┘    └─────────────┘      
src                                     └─────┘    └─────────────┘       
typ                                     └─────┘    └─────────────┘      
doc    └──┘                             └─────┘    └─────────────┘
963  begin
st   └─────
964    by_cases h : a = 0,
id                   
src    └───────┘ └─┘ └┘
typ    └───────┘ └─┘└┘
doc    └───────┘ └─┘  └┘
txt    └───────┘ └─┘  └┘
par    └───────┘ └─┘  └┘
pid             └─┘  
st   ───────────────────┘└─
965    { rw [h, zero_mul, zero_to_real] },
id             └──────┘  └──────────┘
src      └──┘ └┘└──────┘└┘└──────────┘└┘
typ      └──┘└┘└──────┘└┘└──────────┘└┘
doc      └──┘ └┘        └┘            └┘
txt      └──┘ └┘        └┘            └┘
par      └──┘ └┘        └┘            └┘
pid        └┘ └┘        └┘            
st   ───┘└───┘└────────┘└────────────┘└┘
966    { rw [mul_top, if_neg h, top_to_real] }
id           └─────┘  └────┘   └─────────┘
src      └──┘└─────┘└┘└────┘ └┘└─────────┘└┘
typ      └──┘└─────┘└┘└────┘└┘└─────────┘└┘
doc      └──┘       └┘       └┘           └┘
txt      └──┘       └┘       └┘           └┘
par      └──┘       └┘       └┘           └┘
pid        └┘       └┘       └┘           
st   ──────────────┘└────────┘└───────────┘└─
967  end
st   ──┘
968  
969  @[simp] lemma to_real_top_mul (a : ennreal) : ennreal.to_real (⊤ * a) = 0 :=
id                                      └─────┘    └─────────────┘      
src                                     └─────┘    └─────────────┘       
typ                                     └─────┘    └─────────────┘      
doc    └──┘                             └─────┘    └─────────────┘
970  by { rw mul_comm, exact to_real_mul_top _ }
id           └──────┘        └─────────────┘
src       └─┘└──────┘  └────┘└─────────────┘└─┘
typ       └─┘└──────┘  └────┘└─────────────┘└─┘
doc       └─┘          └────┘               └─┘
txt       └─┘          └────┘               └─┘
par       └─┘          └────┘               └─┘
pid                                       └┘
st     └────────────┘└────────────────────────┘└┘
971  
972  lemma to_real_eq_to_real {a b : ennreal} (ha : a < ⊤) (hb : b < ⊤) :
id                                   └─────┘                    
src                                  └─────┘                      
typ                                  └─────┘                    
doc                                  └─────┘
973    ennreal.to_real a = ennreal.to_real b ↔ a = b :=
id     └─────────────┘   └─────────────┘     
src    └─────────────┘    └─────────────┘      
typ    └─────────────┘   └─────────────┘     
doc    └─────────────┘     └─────────────┘
974  begin
st   └─────
975    rw ennreal.lt_top_iff_ne_top at *,
id        └───────────────────────┘
src    └─┘└───────────────────────┘└───┘
typ    └─┘└───────────────────────┘└───┘
doc    └─┘                         └───┘
txt    └─┘                         └───┘
par    └─┘                         └───┘
pid                               └───┘
st   ──────────────────────────────────┘└─
976    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
977    { assume h, apply le_antisymm,
id                       └─────────┘
src      └──────┘  └────┘└─────────┘
typ      └──────┘  └────┘└─────────┘
doc      └──────┘  └────┘
txt      └──────┘  └────┘
par      └──────┘  └────┘
pid      └──────┘       
st   ───┘└──────┘└─────────────────┘└─
978        rw ← to_real_le_to_real ha hb, exact le_of_eq h,
id              └────────────────┘ └┘ └┘        └──────┘ 
src        └───┘└────────────────┘      └────┘└──────┘
typ        └───┘└────────────────┘└┘└┘  └────┘└──────┘
doc        └───┘                        └────┘        
txt        └───┘                        └────┘        
par        └───┘                        └────┘        
pid          └─┘                                     
st   ──────────────────────────────────┘└────────────────┘└─
979        rw ← to_real_le_to_real hb ha, exact le_of_eq h.symm },
id              └────────────────┘ └┘ └┘        └──────┘ └────┘
src        └───┘└────────────────┘      └────┘└──────┘└────┘
typ        └───┘└────────────────┘└┘└┘  └────┘└──────┘└────┘
doc        └───┘                        └────┘              
txt        └───┘                        └────┘              
par        └───┘                        └────┘              
pid          └─┘                                           
st   ──────────────────────────────────┘└──────────────────────┘└┘
980    { assume h, rw h }
id                    
src      └──────┘  └─┘ 
typ      └──────┘  └─┘
doc      └──────┘  └─┘ 
txt      └──────┘  └─┘ 
par      └──────┘  └─┘ 
pid      └──────┘     
st   ───────────┘└─────┘└─
981  end
st   ──┘
982  
983  lemma to_real_mul_to_real {a b : ennreal} :
id                                    └─────┘
src                                   └─────┘
typ                                   └─────┘
doc                                   └─────┘
984    (ennreal.to_real a) * (ennreal.to_real b) = ennreal.to_real (a * b) :=
id      └─────────────┘     └─────────────┘    └─────────────┘    
src     └─────────────┘      └─────────────┘     └─────────────┘    
typ     └─────────────┘     └─────────────┘    └─────────────┘    
doc     └─────────────┘       └─────────────┘      └─────────────┘
985  begin
st   └─────
986    by_cases ha : a = ⊤,
id                     
src    └───────┘  └─┘ 
typ    └───────┘  └─┘
doc    └───────┘  └─┘  
txt    └───────┘  └─┘  
par    └───────┘  └─┘  
pid              └─┘  
st   ────────────────────┘└─
987    { rw ha, simp },
id          └┘
src      └─┘    └───┘
typ      └─┘└┘  └───┘
doc      └─┘    └───┘
txt      └─┘    └───┘
par      └─┘    └───┘
pid                
st   ───┘└───┘└─────┘└┘
988    by_cases hb : b = ⊤,
id                   
src    └───────┘  └─┘  
typ    └───────┘  └─┘ 
doc    └───────┘  └─┘  
txt    └───────┘  └─┘  
par    └───────┘  └─┘  
pid              └─┘  
st   ────────────────────┘└─
989    { rw hb, simp },
id          └┘
src      └─┘    └───┘
typ      └─┘└┘  └───┘
doc      └─┘    └───┘
txt      └─┘    └───┘
par      └─┘    └───┘
pid                
st   ───┘└───┘└─────┘└┘
990    have ha : ennreal.of_real (ennreal.to_real a) = a := of_real_to_real ha,
id               └─────────────┘  └─────────────┘          └─────────────┘ └┘
src    └────────┘└─────────────┘ └─────────────┘ └┘  └──┘└─────────────┘
typ    └────────┘└─────────────┘ └─────────────┘ └┘ └──┘└─────────────┘└┘
doc    └────────┘└─────────────┘ └─────────────┘ └┘  └──┘               
txt    └────────┘                                └┘  └──┘               
par    └────────┘                                └┘  └──┘               
pid    └─────┘└─┘                                └┘  └──┘               
st   ────────────────────────────────────────────────────────────────────────┘└─
991    have hb : ennreal.of_real (ennreal.to_real b) = b := of_real_to_real hb,
id               └─────────────┘  └─────────────┘          └─────────────┘ └┘
src    └────────┘└─────────────┘ └─────────────┘ └┘  └──┘└─────────────┘
typ    └────────┘└─────────────┘ └─────────────┘ └┘ └──┘└─────────────┘└┘
doc    └────────┘└─────────────┘ └─────────────┘ └┘  └──┘               
txt    └────────┘                                └┘  └──┘               
par    └────────┘                                └┘  └──┘               
pid    └─────┘└─┘                                └┘  └──┘               
st   ────────────────────────────────────────────────────────────────────────┘└─
992    conv_rhs { rw [← ha, ← hb, ← of_real_mul to_real_nonneg] },
id                      └┘    └┘    └─────────┘ └────────────┘
src    └─────────┘└────┘  └──┘  └──┘└─────────┘└────────────┘└┘
typ    └─────────┘└────┘└┘└──┘└┘└──┘└─────────┘└────────────┘└┘
txt    └─────────┘└────┘  └──┘  └──┘                         └┘
par    └─────────┘└────┘  └──┘  └──┘                         └┘
pid            └──────┘  └──┘  └──┘                         └─┘
st   ───────────┘└───────┘└────┘└────────────────────────────┘ └┘
993    rw [to_real_of_real (mul_nonneg to_real_nonneg to_real_nonneg)]
id         └─────────────┘  └────────┘                └────────────┘
src    └──┘└─────────────┘ └────────┘              └────────────┘└─┘
typ    └──┘└─────────────┘ └────────┘              └────────────┘└─┘
doc    └──┘                                                      └─┘
txt    └──┘                                                      └─┘
par    └──┘                                                      └─┘
pid      └┘                                                      └┘
st   ───────────────────────────────────────────────────────────────┘
994  end
st   └─┘
995  
996  end real
997  
998  section infi
999  variables {ι : Sort*} {f g : ι → ennreal}
id                                    └─────┘
src                                   └─────┘
typ                                   └─────┘
doc                                   └─────┘
1000  
1001  lemma infi_add : infi f + a = ⨅i, f i + a :=
id                    └──┘         
src                   └──┘             
typ                   └──┘         
doc                   └──┘          
1002  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
1003    (le_infi $ assume i, add_le_add' (infi_le _ _) $ le_refl _)
id      └─────┘            └─────────┘  └─────┘        └─────┘
src     └─────┘             └─────────┘  └─────┘        └─────┘
typ     └─────┘            └─────────┘  └─────┘        └─────┘
1004    (ennreal.sub_le_iff_le_add.1 $ le_infi $ assume i, ennreal.sub_le_iff_le_add.2 $ infi_le _ _)
id      └───────────────────────┘    └─────┘            └───────────────────────┘    └─────┘
src     └───────────────────────┘    └─────┘             └───────────────────────┘    └─────┘
typ     └───────────────────────┘    └─────┘            └───────────────────────┘    └─────┘
1005  
1006  lemma supr_sub : (⨆i, f i) - a = (⨆i, f i - a) :=
id                                 
src                                      
typ                                
doc                                   
1007  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
1008    (ennreal.sub_le_iff_le_add.2 $ supr_le $ assume i, ennreal.sub_le_iff_le_add.1 $ le_supr _ i)
id      └───────────────────────┘    └─────┘            └───────────────────────┘    └─────┘   
src     └───────────────────────┘    └─────┘             └───────────────────────┘    └─────┘
typ     └───────────────────────┘    └─────┘            └───────────────────────┘    └─────┘   
1009    (supr_le $ assume i, ennreal.sub_le_sub (le_supr _ _) (le_refl a))
id      └─────┘            └────────────────┘  └─────┘       └─────┘ 
src     └─────┘             └────────────────┘  └─────┘       └─────┘
typ     └─────┘            └────────────────┘  └─────┘       └─────┘ 
1010  
1011  lemma sub_infi : a - (⨅i, f i) = (⨆i, a - f i) :=
id                                 
src                                    
typ                                
doc                                   
1012  begin
st   └─────
1013    refine (eq_of_forall_ge_iff $ λ c, _),
id             └─────────────────┘
src    └─────┘ └─────────────────┘  └────┘
typ    └─────┘ └─────────────────┘  └────┘
doc    └─────┘                      └────┘
txt    └─────┘                      └────┘
par    └─────┘                      └────┘
pid                                └────┘
st   ──────────────────────────────────────┘└─
1014    rw [ennreal.sub_le_iff_le_add, add_comm, infi_add],
id         └───────────────────────┘  └──────┘  └──────┘
src    └──┘└───────────────────────┘└┘└──────┘└┘└──────┘
typ    └──┘└───────────────────────┘└┘└──────┘└┘└──────┘
doc    └──┘                         └┘        └┘        
txt    └──┘                         └┘        └┘        
par    └──┘                         └┘        └┘        
pid      └┘                         └┘        └┘        
st   ──────────────────────────────┘└────────┘└────────┘└──
1015    simp [ennreal.sub_le_iff_le_add]
id           └───────────────────────┘
src    └────┘└───────────────────────┘└┘
typ    └────┘└───────────────────────┘└┘
doc    └────┘                         └┘
txt    └────┘                         └┘
par    └────┘                         └┘
pid                                 
st   ──────────────────────────────────┘
1016  end
st   └─┘
1017  
1018  lemma Inf_add {s : set ennreal} : Inf s + a = ⨅b∈s, b + a :=
id                      └─┘ └─────┘    └─┘         
src                     └─┘ └─────┘    └─┘             
typ                     └─┘ └─────┘    └─┘         
doc                         └─────┘    └─┘            
1019  by simp [Inf_eq_infi, infi_add]
id            └─────────┘  └──────┘
src     └────┘└─────────┘└┘└──────┘└─
typ     └────┘└─────────┘└┘└──────┘└─
doc     └────┘           └┘        └─
txt     └────┘           └┘        └─
par     └────┘           └┘        └─
pid                    └┘        
st     └─────────────────────────────
1020  
src  
typ  
doc  
txt  
par  
pid  
st   
1021  lemma add_infi {a : ennreal} : a + infi f = ⨅b, a + f b :=
id                       └─────┘      └──┘       
src                      └─────┘       └──┘        
typ                      └─────┘      └──┘       
doc                      └─────┘        └──┘      
1022  by rw [add_comm, infi_add]; simp
id          └──────┘  └──────┘
src     └──┘└──────┘└┘└──────┘  └────
typ     └──┘└──────┘└┘└──────┘  └────
doc     └──┘        └┘          └────
txt     └──┘        └┘          └────
par     └──┘        └┘          └────
pid       └┘        └┘              
st     └───────────┘└────────┘└──────
1023  
src  
typ  
doc  
txt  
par  
pid  
st   
1024  lemma infi_add_infi (h : ∀i j, ∃k, f k + g k ≤ f i + g j) : infi f + infi g = (⨅a, f a + g a) :=
id                                               └──┘   └──┘         
src                                                         └──┘    └──┘           
typ                                              └──┘   └──┘         
doc                                                              └──┘     └──┘       
1025  suffices (⨅a, f a + g a) ≤ infi f + infi g,
id                     └──┘   └──┘ 
src                         └──┘    └──┘
typ                    └──┘   └──┘ 
doc                           └──┘     └──┘
1026    from le_antisymm (le_infi $ assume a, add_le_add' (infi_le _ _) (infi_le _ _)) this,
id          └─────────┘  └─────┘            └─────────┘  └─────┘       └─────┘       └──┘
src         └─────────┘  └─────┘             └─────────┘  └─────┘       └─────┘
typ         └─────────┘  └─────┘            └─────────┘  └─────┘       └─────┘       └──┘
1027  calc (⨅a, f a + g a) ≤ (⨅ a a', f a + g a') :
id                     └┘     └┘
src                                 
typ                    └┘     └┘
doc                             
1028      le_infi $ assume a, le_infi $ assume a',
id       └─────┘            └─────┘          └┘
src      └─────┘             └─────┘
typ      └─────┘            └─────┘          └┘
1029        let ⟨k, h⟩ := h a a' in infi_le_of_le k h
id         └─┘           └┘    └───────────┘
src                                └───────────┘
typ        └─┘           └┘    └───────────┘
1030    ... ≤ infi f + infi g :
id           └──┘   └──┘ 
src          └──┘    └──┘
typ          └──┘   └──┘ 
doc          └──┘     └──┘
1031      by simp [add_infi, infi_add, -add_comm, -le_infi_iff]; exact le_refl _
id                └──────┘  └──────┘                                  └─────┘
src         └────┘└──────┘└┘└──────┘└────────────────────────┘  └────┘└─────┘└──
typ         └────┘└──────┘└┘└──────┘└────────────────────────┘  └────┘└─────┘└──
doc         └────┘        └┘        └────────────────────────┘  └────┘       └──
txt         └────┘        └┘        └────────────────────────┘  └────┘       └──
par         └────┘        └┘        └────────────────────────┘  └────┘       └──
pid                     └┘        └────────────────────────┘              └┘
st         └────────────────────────────────────────────────────────────────────
1032  
src  
typ  
doc  
txt  
par  
pid  
st   
1033  lemma infi_sum {f : ι → α → ennreal} {s : finset α} [nonempty ι]
id                             └─────┘       └────┘    └──────┘ 
src                              └─────┘       └────┘     └──────┘
typ                            └─────┘       └────┘    └──────┘ 
doc                              └─────┘       └────┘
1034    (h : ∀(t : finset α) (i j : ι), ∃k, ∀a∈t, f k a ≤ f i a ∧ f k a ≤ f j a) :
id                └────┘                                
src               └────┘                                           
typ               └────┘                                
doc               └────┘
1035    (⨅i, s.sum (f i)) = s.sum (λa, ⨅i, f i a) :=
id       └──┘       └──┘        
src        └──┘          └──┘       
typ      └──┘       └──┘        
doc                                  
1036  finset.induction_on s (by simp) $ assume a s ha ih,
id   └─────────────────┘                       └┘ └┘
src  └─────────────────┘       └──┘
typ  └─────────────────┘      └──┘             └┘ └┘
doc  └─────────────────┘       └──┘
txt                            └──┘
par                            └──┘
st                            └───┘
1037    have ∀ (i j : ι), ∃ (k : ι), f k a + s.sum (f k) ≤ f i a + s.sum (f j),
id                                  └──┘          └──┘   
src                                       └──┘                └──┘
typ                                 └──┘          └──┘   
1038      from assume i j,
id                    
typ                   
1039      let ⟨k, hk⟩ := h (insert a s) i j in
id       └─┘    └┘       └────┘     
src                        └────┘
typ      └─┘    └┘       └────┘     
1040      ⟨k, add_le_add' (hk a (finset.mem_insert_self _ _)).left $ finset.sum_le_sum $
id           └─────────┘       └────────────────────┘      └──┘    └───────────────┘
src          └─────────┘        └────────────────────┘      └──┘    └───────────────┘
typ          └─────────┘       └────────────────────┘      └──┘    └───────────────┘
1041        assume a ha, (hk _ $ finset.mem_insert_of_mem ha).right⟩,
id                 └┘          └──────────────────────┘ └┘ └───┘
src                             └──────────────────────┘    └───┘
typ                └┘          └──────────────────────┘ └┘ └───┘
1042    by simp [ha, ih.symm, infi_add_infi this]
id              └┘           └───────────┘ └──┘
src       └────┘  └┘       └┘└───────────┘    └─
typ       └────┘└┘└┘└─────┘└┘└───────────┘└──┘└─
doc       └────┘  └┘       └┘                 └─
txt       └────┘  └┘       └┘                 └─
par       └────┘  └┘       └┘                 └─
pid             └┘       └┘                 
st       └───────────────────────────────────────
1043  
src  
typ  
doc  
txt  
par  
pid  
st   
1044  end infi
1045  
1046  section supr
1047  
1048  lemma supr_coe_nat : (⨆n:ℕ, (n : ennreal)) = ⊤ :=
id                                └─────┘    
src                                └─────┘    
typ                               └─────┘    
doc                                 └─────┘
1049  (lattice.supr_eq_top _).2 $ assume b hb, ennreal.exists_nat_gt (lt_top_iff_ne_top.1 hb)
id    └─────────────────┘               └┘  └───────────────────┘  └───────────────┘  └┘
src   └─────────────────┘                    └───────────────────┘  └───────────────┘
typ   └─────────────────┘               └┘  └───────────────────┘  └───────────────┘  └┘
1050  
1051  end supr
1052  
1053  end ennreal